proposition: Theorem le_plus_n_m : forall n m : nat, n <= m -> n + n <= m + m.
proof: Proof. simple induction n. auto with arith. intros. inversion H0. auto with arith. simpl in |- *. elim plus_n_Sm. elim plus_n_Sm. apply le_n_S. apply le_n_S. apply H. apply le_Sn_le. exact H1. Qed.
imports: Plus Mult Minus Lt Le Gt