proposition: Theorem le_alt_dichotomy : forall n m, le_alt n m \/ le_alt m n.
proof: Proof. intros n m; induct n. - left; exists m; apply add_0_r. - intros n IH. destruct IH as [[p H] | [p H]]. + destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H. * rewrite add_0_l in H. right; exists (S 0); rewrite H, add_succ_l; now rewrite add_0_l. * left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H. + right; exists (S p). rewrite add_succ_l; now rewrite H. Qed.
imports: NMulOrder