PartialOrder (≤) | 10. Proof. repeat split. - apply _. - apply _. - intros x. apply not_lt_le_flip, (irreflexivity (<)). - intros x y z E1 E2. apply le_iff_not_lt_flip; apply le_iff_not_lt_flip in E1; apply le_iff_not_lt_flip in E2. change (complement (<) z x). transitivity y;assumption. - intros x y E1 E2. apply le_iff_not_lt_flip in E1; apply le_iff_not_lt_flip in E2. apply (antisymmetry (complement (<)));assumption. Qed.
Require Import