proposition: Lemma f_strext: (fun_strext (f is_generated_by)).
proof: Proof. unfold fun_strext; simpl. induction x; destruct y. - intros ? ?. pose proof (ax_ap_irreflexive M (@cs_eq M) (@cs_ap M)) as H_irreflexive. unfold irreflexive, Not in H_irreflexive. elim H_irreflexive with (cm_unit M); auto using CSetoid_is_CSetoid. - firstorder lia. - firstorder lia. - unfold f. simpl. elim (@csg_op M). simpl. intros op op_strext H1. pose proof (op_strext c c (power_CMonoid c _) (power_CMonoid c _) H1) as [ H3 | ]. + destruct (ap_irreflexive_unfolded M c H3). + firstorder. Qed.
imports: Lia CoRN.algebra.CMonoids CoRN.model.monoids.Nmonoid