proposition: Theorem le_dec : ∀ (n m : Nbar), {n ≤ m} + {~ n ≤ m}.
proof: Proof. intros n m. destruct n as [n| ]. destruct m as [m| ]. destruct (le_dec n m) as [Hlt| Hge]. left; constructor; assumption. right; intros H; apply Hge; clear Hge. inversion H; assumption. left; constructor. destruct m as [m| ]; [ right; intros H; inversion H | idtac ]. left; constructor. Qed.
imports: Utf8 Compare_dec NPeano Misc