proposition: Theorem lt_1_r : forall n, n < 1 <-> n == 0.
proof: Proof. setoid_rewrite one_succ. intro n; cases n. - split; intro; [reflexivity | apply lt_succ_diag_r]. - intros n. rewrite <- succ_lt_mono. split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0]. Qed.
imports: NAdd