proposition: Theorem lt_plus_n_m : forall n m : nat, n < m -> S (n + n) < m + m.
proof: Proof. simple induction n. simpl in |- *. simple induction m. simpl in |- *. intros. absurd (0 < 0). apply le_not_lt. auto with arith. exact H. intros. simpl in |- *. elim plus_n_Sm. apply lt_n_S. auto with arith. intros. inversion H0. simpl in |- *. repeat elim plus_n_Sm. auto with arith. simpl in |- *. repeat elim plus_n_Sm. apply lt_n_S. apply lt_n_S. apply H. inversion H1. auto with arith. apply le_lt_n_Sm. apply le_Sn_le. apply le_Sn_le. exact H3. Qed.
imports: Plus Mult Minus Lt Le Gt