From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- theories/Arith/Plus.v | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) mode change 100755 => 100644 theories/Arith/Plus.v (limited to 'theories/Arith/Plus.v') diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v old mode 100755 new mode 100644 index e4ac631e..56e1c58a --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Plus.v,v 1.18.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) +(*i $Id: Plus.v 8642 2006-03-17 10:09:02Z notin $ i*) (** Properties of addition *) @@ -199,4 +199,29 @@ Definition tail_plus n m := plus_acc m n. Lemma plus_tail_plus : forall n m, n + m = tail_plus n m. unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto. intro m; rewrite <- IHn; simpl in |- *; auto. -Qed. \ No newline at end of file +Qed. + +(** Discrimination *) + +Lemma succ_plus_discr : forall n m, n <> S (plus m n). +Proof. +intros n m; induction n as [|n IHn]. + discriminate. + intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; + reflexivity. +Qed. + +Lemma n_SSn : forall n, n <> S (S n). +Proof. +intro n; exact (succ_plus_discr n 1). +Qed. + +Lemma n_SSSn : forall n, n <> S (S (S n)). +Proof. +intro n; exact (succ_plus_discr n 2). +Qed. + +Lemma n_SSSSn : forall n, n <> S (S (S (S n))). +Proof. +intro n; exact (succ_plus_discr n 3). +Qed. -- cgit v1.2.3