diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-03 08:24:34 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-03 08:24:34 +0000 |
| commit | 288c8de205667afc00b340556b0b8c98ffa77459 (patch) | |
| tree | 40c77b6c241ed39ce64e59ead13b35bd57d7c299 /theories/Numbers/Natural/Abstract/NIso.v | |
| parent | 4ade23ef522409d0754198ea35747a65b6fa9d81 (diff) | |
Numbers: start using Classes stuff, Equivalence, Proper, Instance, etc
TODO: finish removing the "Add Relation", "Add Morphism" fun_* fun2_*
TODO: now that we have Include, flatten the hierarchy...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12464 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NIso.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NIso.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 5ad343fe0..da48d2fe0 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ : forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n). Proof. unfold natural_isomorphism. -intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ; -[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd]. +intro n. rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq); auto with *. +repeat red; intros. apply NBasePropMod2.succ_wd; auto. Qed. Theorem hom_nat_iso : homomorphism natural_isomorphism. |