proposition: Theorem eq_pred_0 n : P n == 0 <-> n == 0 \/ n == 1.
proof: Proof. cases n. - rewrite pred_0. now split; [left|]. - intro n. rewrite pred_succ. split. + intros H; right. now rewrite H, one_succ. + intros [H|H]. * elim (neq_succ_0 _ H). * apply succ_inj_wd. now rewrite <- one_succ. Qed.
imports: Decidable NAxioms NZProperties