proposition: Lemma unit_commMonoidLaws : comMonoidLaws tt (fun _ _ => tt).
proof: Proof. by do 2 (split; try done). Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)