proposition: Lemma lt_irrefl : Irreflexive lt.
proof: Proof. assert (HIP : Irreflexive Pos.lt) by (apply StrictOrder_Irreflexive; assumption). unfold Irreflexive in *. unfold Reflexive in *. unfold complement in *. intro x. unfold lt. assert (HEq : Pos.eqb (fstpp(x)) (fstpp(x)) = true) by (apply Pos.eqb_eq; intuition). rewrite HEq. apply HIP. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms