Require Export Arith.
Require Export Even.
Require Export Div2.
Require Export ZArith.
Lemma lt_minus_1 :forall n:nat, 0<n -> n-1<n.
intros n h;omega.
Qed.
Definition sqr := fun x:Z => (x*x)%Z.
| More lemmas about even and odd |
Lemma odd_even_minus : forall m:nat, 0<m -> odd m -> even (m-1).
intros m Hm Hodd.
inversion Hodd.
simpl.
rewrite <- minus_n_O.
apply H.
Qed.
| arithmetic lemmas |
Lemma not_zero_implies_pos_or_neg : forall a:Z, (a<>0)%Z->(a<0)%Z\/(0<a)%Z.
intros a; elim a.
unfold not.
intros V.
cut False.
intros Hf;elim Hf.
apply V.
trivial.
intros p H ; right.
unfold Zlt;simpl;trivial.
intros p H ; left.
unfold Zlt;simpl;trivial.
Qed.
Lemma not_zero_implies_square_pos : forall a:Z, (a<>0)%Z -> (0<a*a)%Z.
intros a h.
elim (not_zero_implies_pos_or_neg a h).
intros h1.
replace (a*a)%Z with ((-a)*(-a))%Z; [idtac|ring].
apply Zmult_lt_O_compat;omega.
intros h2.
apply Zmult_lt_O_compat;omega.
Qed.
| sign of the product of integers |
Lemma signe1 : forall a b:Z, (a<0)%Z -> (0<b)%Z ->(a*b<0)%Z.
intros a b Ha Hb.
replace 0%Z with (0*b)%Z; [idtac|ring].
apply Zmult_lt_compat_r;assumption.
Qed.
Lemma signe2 : forall a b:Z, (0<a)%Z -> (0<b)%Z ->(0<a*b)%Z.
intros a b Ha Hb.
replace 0%Z with (0*b)%Z; [idtac|ring].
apply Zmult_lt_compat_r;assumption.
Qed.
Lemma signe3 : forall a b:Z, (a<0)%Z -> (b<0)%Z ->(0<a*b)%Z.
intros a b Ha Hb.
replace (a*b)%Z with ((-a)*(-b))%Z; [idtac|ring].
replace 0%Z with ((-a)*0)%Z; [idtac|ring].
apply Zmult_gt_0_lt_compat_l.
omega.
omega.
Qed.
Lemma signe4 : forall a b:Z, (0<a)%Z -> (b<0)%Z ->(a*b<0)%Z.
intros a b Ha Hb.
replace (a*b)%Z with ((-a)*(-b))%Z; [idtac|ring].
replace 0%Z with (0*(-b))%Z; [idtac|ring].
apply Zmult_gt_0_lt_compat_r.
omega.
omega.
Qed.
Lemma mult_diff : forall a b:Z, (a<>0)%Z->(b<>0)%Z ->(a*b<>0)%Z.
intros a b Ha Hb.
cut ((a<0)%Z\/(0<a)%Z); [idtac|omega].
cut ((b<0)%Z\/(0<b)%Z); [idtac|omega].
intros H1 H2.
elim H1; intros H3.
elim H2; intros H4.
cut (0<a*b)%Z; [omega|idtac].
apply signe3;assumption.
cut (a*b<0)%Z; [omega|idtac].
apply signe4;assumption.
elim H2; intros H4.
cut (a*b<0)%Z;[omega|idtac].
apply signe1;assumption.
cut (0<a*b)%Z;[omega|idtac].
apply signe2;assumption.
Qed.