proposition: Lemma iso_inv: (isomorphism M2 M1 (Inv f (iso_imp_bij))).
proof: Proof. unfold isomorphism. split. unfold morphism. split. unfold isomorphism in isof. unfold morphism in isof. elim isof. intros H0 H1. elim H0. clear H0. intros H3 H4. astepl ((Inv f iso_imp_bij) (f [0])). unfold Inv. simpl. apply inv2. intros a b. elim isof. intros H0 H1. destruct H1 as [H1 H2]. destruct (H2 a) as [a' fa'a]. destruct (H2 b) as [b' fb'b]. unfold morphism in H0. astepl ((Inv f iso_imp_bij) (f a' [+] f b')). astepl ((Inv f iso_imp_bij) ( f ( a'[+] b'))). set (H3:= (inv2 M1 M2 f iso_imp_bij (a'[+]b'))). astepl (a'[+]b'). astepr (a'[+] b'). intuition. set (H4:=(inv2 M1 M2 f iso_imp_bij a')). apply csbf_wd. astepr (Inv f iso_imp_bij (f a')); intuition. astepr (Inv f iso_imp_bij (f b')). set (H5:= (inv2 M1 M2 f iso_imp_bij b')); intuition. intuition. apply Inv_bij. Qed.
imports: Coq.Arith.Euclid CoRN.model.Zmod.Cmod CoRN.algebra.CSemiGroups CoRN.tactics.csetoid_rewrite CoRN.model.structures.Nsec CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms