proposition: Lemma leb_dec : forall p1 p2, leb p1 p2 = true \/ leb p1 p2 = false.
proof: Proof. intros. elim Pos.eq_dec with p1 p2. intro; subst. left; apply POrderedType.Positive_as_DT.leb_refl. intro HNeq. elim leb_total with p1 p2; intro Hp1p2. left; assumption. right. rewrite Positive_as_DT.leb_gt. rewrite Positive_as_DT.leb_le in Hp1p2. rewrite Pos.lt_eq_cases in Hp1p2. elim Hp1p2; intro. assumption. subst; intuition. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms