proposition: Lemma le_le_mult : forall b a c d : nat, a <= b -> c <= d -> a * c <= b * d.
proof: Proof. simple induction b. intros. replace a with 0. simpl in |- *. apply le_n. apply le_n_O_eq. assumption. intros b1 IHb1. simpl in |- *. intros. elim (le_lt_or_eq a (S b1)). unfold lt in |- *. intros. rewrite (plus_comm d (b1 * d)). apply le_plus_trans. apply IHb1. apply le_S_n. assumption. assumption. intro. rewrite H1. replace (d + b1 * d) with (S b1 * d). apply le_mult_l. assumption. reflexivity. assumption. Qed.
imports: ZArith EqNat