proposition: Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) : StrictOrder (relation_conjunction R (complement eqA)).
proof: Proof. split; compute. - intros x (_,Hx). apply Hx, Equivalence_Reflexive. - intros x y z (Hxy,Hxy') (Hyz,Hyz'). split. + apply PreOrder_Transitive with y; assumption. + intro Hxz. apply Hxy'. apply partial_order_antisym; auto. rewrite Hxz; auto. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses