diff options
author | 2011-01-03 18:51:13 +0000 | |
---|---|---|
committer | 2011-01-03 18:51:13 +0000 | |
commit | 8e2d90a6a9f4480026afd433fc997d9958f76a38 (patch) | |
tree | 6a92d154766a3a8934b91705acf79cc994a42061 /theories/Numbers/Natural/Abstract/NSub.v | |
parent | 05662999c9ab0183c0f97fc18579379142ac7b38 (diff) |
Numbers: some improvements in proofs
- a ltac solve_proper which generalizes solve_predicate_wd and co
- using le_elim is nicer that (apply le_lteq; destruct ...)
- "apply ->" can now be "apply" most of the time.
Benefit: NumPrelude is now almost empty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NSub.v')
-rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index 4232ecbfa..d7143c677 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -35,7 +35,7 @@ Qed. Theorem sub_gt : forall n m, n > m -> n - m ~= 0. Proof. intros n m H; elim H using lt_ind_rel; clear n m H. -solve_relation_wd. +solve_proper. intro; rewrite sub_0_r; apply neq_succ_0. intros; now rewrite sub_succ. Qed. @@ -45,8 +45,8 @@ Proof. intros n m p; induct p. intro; now do 2 rewrite sub_0_r. intros p IH H. do 2 rewrite sub_succ_r. -rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). -rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l). +rewrite <- IH by (apply lt_le_incl; now apply le_succ_l). +rewrite add_pred_r by (apply sub_gt; now apply le_succ_l). reflexivity. Qed. @@ -242,10 +242,10 @@ intros n IH. destruct (le_gt_cases m n) as [H | H]. rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l. rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. -now apply <- add_cancel_l. -assert (H1 : S n <= m); [now apply <- le_succ_l |]. -setoid_replace (S n - m) with 0 by now apply <- sub_0_le. -setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r). +now apply add_cancel_l. +assert (H1 : S n <= m); [now apply le_succ_l |]. +setoid_replace (S n - m) with 0 by now apply sub_0_le. +setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r). apply mul_0_l. Qed. |