proposition: Theorem pred_le_mono : forall n m, n <= m -> P n <= P m.
proof: Proof. intros n m H; elim H using le_ind_rel. - solve_proper. - intro; rewrite pred_0; apply le_0_l. - intros p q H1 _; now do 2 rewrite pred_succ. Qed.
imports: NAdd