proposition: Lemma isnat_mult : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (0 <= x * y)%Z.
proof: Proof. simple induction x. simpl in |- *. intros. unfold Z.le in |- *. simpl in |- *. discriminate. intro. simple induction y. simpl in |- *. intros. unfold Z.le in |- *. simpl in |- *. discriminate. simpl in |- *. intros. unfold Z.le in |- *. simpl in |- *. discriminate. intros. unfold Z.le in H0. elim H0. simpl in |- *. reflexivity. intros. unfold Z.le in H. elim H. simpl in |- *. reflexivity. Qed.
imports: ZArith EqNat lemmas