proposition: Lemma CProper2: Proper (i R ==> i S ==> i T) g.
proof: Proof. intros x y [E] u v [F]. exists. by apply Hg. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)