proposition: Theorem le_0_l : forall n, 0 <= n.
proof: Proof. intro n; nzinduct n. - now apply eq_le_incl. - intro n; split. + apply le_le_succ_r. + intro H; apply le_succ_r in H; destruct H as [H | H]. * assumption. * symmetry in H; false_hyp H neq_succ_0. Qed.
imports: Decidable NAxioms NZProperties