proposition: Lemma lt_trans : Transitive lt.
proof: Proof. assert (HTP : Transitive Pos.lt) by (apply StrictOrder_Transitive; assumption). unfold Transitive in *. intros x y z. unfold lt. case_eq (Pos.eqb (fstpp(x)) (fstpp(y))). intro HEqXY. case_eq (Pos.eqb (fstpp(y)) (fstpp(z))). intro HEqYZ. assert (HEqXZ : Pos.eqb (fstpp(x)) (fstpp(z)) = true) by (apply Pos.eqb_eq in HEqXY; rewrite HEqXY; assumption). rewrite HEqXZ. apply HTP. intro HNEqYZ. assert (HNEqXZ : Pos.eqb (fstpp(x)) (fstpp(z)) = false) by (apply Pos.eqb_eq in HEqXY; rewrite HEqXY; assumption). rewrite HNEqXZ. apply Pos.eqb_eq in HEqXY; rewrite HEqXY. intro. intuition. intro HNEqXY. case_eq (Pos.eqb (fstpp(y)) (fstpp(z))). intro HEqYZ. assert (HNEqXZ : Pos.eqb (fstpp(x)) (fstpp(z)) = false) by (apply Pos.eqb_eq in HEqYZ; rewrite <- HEqYZ; assumption). rewrite HNEqXZ. apply Pos.eqb_eq in HEqYZ; rewrite HEqYZ. intros. assumption. intro HNEqYZ. case_eq (Pos.eqb (fstpp(x)) (fstpp(z))). intro HEqXZ. intros. assert (HLtXZ : Pos.ltb (fstpp(x)) (fstpp(z)) = true) by (apply Pos.ltb_lt; apply HTP with (fstpp(y)); assumption). apply Pos.eqb_eq in HEqXZ; rewrite HEqXZ in HLtXZ. assert (HIP : Irreflexive Pos.lt) by (apply StrictOrder_Irreflexive; assumption). unfold Irreflexive in HIP. unfold Reflexive in HIP. unfold complement in HIP. exfalso. apply HIP with (fstpp(z)). apply Pos.ltb_lt in HLtXZ. assumption. intro HNEqXZ. intros. apply HTP with (fstpp(y)); assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms