proposition: Lemma induced_mor_iff2 {T : Type} (P R : relation T) m : PreOrder P -> InducedSym P R -> Proper (P ==> P --> impl) m -> Proper (R ==> R ==> iff) m.
proof: Proof. intros pre ind prop x y Rxy x' y' Rxy'. apply induced_iff in Rxy. apply induced_iff in Rxy'. destruct Rxy as [Pxy Pyx]. destruct Rxy' as [Pxy' Pyx']. generalize (prop _ _ Pxy _ _ Pyx'). generalize (prop _ _ Pyx _ _ Pxy'). firstorder. Qed.
imports: Setoid Morphisms Basics