proposition: Lemma leb_total : forall p1 p2, leb p1 p2 = true \/ leb p2 p1 = true.
proof: Proof. intros. do 2 (rewrite Pos.leb_le). do 2 (rewrite Pos.le_lteq). assert (HElim := Pos.lt_total p1 p2). elim HElim; clear HElim; intro HElim. left; left; assumption. elim HElim; clear HElim; intro HElim. left; right; assumption. right; left; assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms