proposition: Lemma monUl_of_com : (forall x, mon2 x mon0 ≡ x) -> (forall x y, mon2 x y ≡ mon2 y x) -> forall x, mon2 mon0 x ≡ x.
proof: Proof. move => monU monC x. by rewrite monC monU. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)