proposition: Lemma StrictOrder_PreOrder `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iffT) R) : PreOrder (relation_disjunction R eqA).
proof: Proof. split. - intros x. right. reflexivity. - intros x y z [Hxy|Hxy] [Hyz|Hyz]. + left. transitivity y; auto. + left. rewrite <- Hyz; auto. + left. rewrite Hxy; auto. + right. transitivity y; auto. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses Relation_Definitions