proposition: Theorem pred_lt_mono : forall n m, n ~= 0 -> (n < m <-> P n < P m).
proof: Proof. intros n m H1; split; intro H2. - assert (m ~= 0). { apply neq_0_lt_0. now apply lt_lt_0 with n. } now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ; [apply succ_lt_mono | | |]. - assert (m ~= 0). { apply neq_0_lt_0. apply lt_lt_0 with (P n). apply lt_le_trans with (P m). - assumption. - apply le_pred_l. } apply succ_lt_mono in H2. now do 2 rewrite succ_pred in H2. Qed.
imports: NAdd