proposition: Lemma weakly_inj1: forall (M:CMonoid)(u:M)(k l a b:nat),(is_generator M u)->(a<l)->(b<l)-> (k<l and (power_CMonoid u k [=] power_CMonoid u l) and (forall (k0 l0:nat),k0<>l0 and (k0<k or (k0=k and l0<l))-> (power_CMonoid u k0 [#] power_CMonoid u l0)))-> (power_CMonoid u a)[=](power_CMonoid u b) -> a=b.
proof: Proof. intros M u k l a b H H0 H1. unfold is_generator in H. intros H3 H4. elim (eq_nat_dec a b). tauto. intro H5. elim (not_or a b H5). clear H5. intro H5. cut False. intuition. set (H6:= (eq_imp_not_ap M (power_CMonoid u a)(power_CMonoid u b) H4)). unfold Not in H6. cut (k<>a+(l-b) or k=a+(l-b)). intro orex. elim orex. clear orex. intro orex. cut ((power_CMonoid u a[#]power_CMonoid u b) or (power_CMonoid u (l-b)[#]power_CMonoid u (l-b))). intro H7. elim H7. tauto. clear H7. intro H7. set (H8:= (ap_irreflexive_unfolded M (power_CMonoid u (l-b)) H7)). intuition. apply bin_op_strext_unfolded with (@csg_op M). csetoid_rewrite_rev (power_plus M u b (l-b)). csetoid_rewrite_rev (power_plus M u a (l-b)). elim H3. clear H3. intros H3 H7. elim H7. clear H7. intros H7 H8. replace (b+(l-b)) with l. csetoid_rewrite_rev H7. apply: ap_symmetric. apply H8. split. intuition. right. intuition. intuition. clear orex. intro orex. intuition. intuition. clear H5. intro H5. cut False. intuition. cut (power_CMonoid (M:=M) u b[=]power_CMonoid (M:=M) u a). intro H4'. set (H6:= (eq_imp_not_ap M (power_CMonoid u a)(power_CMonoid u b) H4)). set (H6':= (eq_imp_not_ap M (power_CMonoid u b)(power_CMonoid u a) H4')). unfold Not in H6. cut (k<>b+(l-a) or k=b+(l-a)). intro orex. elim orex. clear orex. intro orex. cut ((power_CMonoid u a[#]power_CMonoid u b) or (power_CMonoid u (l-a)[#]power_CMonoid u (l-a))). intro H7. elim H7. tauto. clear H7. intro H7. set (H8:= (ap_irreflexive_unfolded M (power_CMonoid u (l-a)) H7)). intuition. apply bin_op_strext_unfolded with (@csg_op M). csetoid_rewrite_rev (power_plus M u b (l-a)). csetoid_rewrite_rev (power_plus M u a (l-a)). elim H3. clear H3. intros H3 H7. elim H7. clear H7. intros H7 H8. replace (a+(l-a)) with l. csetoid_rewrite_rev H7. apply H8. split. intuition. right. intuition. intuition. clear orex. intro orex. intuition. intuition. 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