proposition: Lemma simpl_lt_mult_l : forall a b c : nat, a * b < a * c -> b < c.
proof: Proof. simple induction a. simpl in |- *. intros. elim (lt_irrefl 0). assumption. intros a1 IH. intros. elim (le_or_lt b c). intro. elim (le_lt_or_eq b c). intro. assumption. intros. rewrite H1 in H. elim (lt_irrefl (S a1 * c)). assumption. assumption. intros. cut (S a1 * c <= S a1 * b). intros. elim (le_not_lt (S a1 * c) (S a1 * b)). assumption. assumption. apply lt_le_weak. apply lt_mult_l. assumption. Qed.
imports: ZArith EqNat