proposition: Lemma f_strext': (fun_strext f ).
proof: Proof. unfold fun_strext. simpl. intros x y. case x. intros x1 x2. case y. intros y1 y2. simpl. intuition. 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