proposition: Lemma CProper1: Proper (i R ==> i S) f.
proof: Proof. intros x y [H]. exists. by apply Hf. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)