proposition: Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m.
proof: Proof. intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m two). - rewrite two_succ. nzsimpl. now rewrite le_succ_l. - order'. Qed.
imports: NZAxioms NZAddOrder