proposition: Lemma ltListIrrefl : forall l, ltList l l -> False.
proof: Proof. intro l. induction l. simpl; intuition. assert (H := Pos.lt_irrefl a). rewrite <- Pos.ltb_nlt in H. simpl. rewrite H. apply IHl. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms