proposition: Lemma monotone_transp A B (R : rel A) (S : rel B) f : monotone R S f -> monotone (transp R) (transp S) f.
proof: Proof. unfold monotone, transp. auto. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)