proposition: Lemma lt_antiref : forall x, ~ lt x x.
proof: Proof. assert (HIL : Irreflexive lt) by (apply lt_irrefl). unfold Irreflexive in *. unfold Reflexive in *. unfold complement in *. intros x H. apply HIL with x. apply H. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms