proposition: Lemma StrictOrder_PartialOrder `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iffT) R) : PartialOrder eqA (relation_disjunction R eqA).
proof: Proof. intros. intros x y. compute. intuition auto with crelations. elim (StrictOrder_Irreflexive x). transitivity y; auto. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses Relation_Definitions