Library AreaMethod.field_general_properties

Require Export field_variable_isolation_tactic.


Lemma field_prop_1 : forall a b : F, a + b = a -> b = 0.
Proof with try solve [ ring | congruence ].
intros...
assert (a + b - a = a - a)...
assert (a - a = 0)...
rewrite H1 in H0...
assert (a + b - a = b)...
Qed.

Lemma field_prop_3 : forall a : F, a = 0 -> - a = 0.
intros.
rewrite H.
ring.
Qed.

Lemma field_prop_4 : forall a : F, - a = 0 -> a = 0.
Proof with try solve [ ring | congruence ].
intros...
assert (a + - a = a + 0)...
assert (a + - a = 0)...
rewrite H1 in H0...
assert (a + 0 = a)...
Qed.

Lemma field_prop_5 : forall a b : F, - a = - b -> a = b.
Proof with try solve [ ring | congruence ].
intros...
assert (- - a = - - b)...
assert (- - a = a)...
assert (- - b = b)...
Qed.

Lemma nonzeromult : forall a b : F, a <> 0 -> b <> 0 -> a * b <> 0.
Proof with try solve [ auto with field_hints | congruence ].
intros...
assert (a * b / b = a)...
field...
intuition...
assert (a * b / b = 0 / b)...
rewrite H1 in H3...
assert (a = 0)...
assert (0 / b = 0)...
field...
Qed.

Lemma nonzerodiv : forall a b : F, a <> 0 -> b <> 0 -> a / b <> 0.
Proof with try solve [ auto with field_hints | congruence ].
intros...
unfold not in |- *; intro...
IsoleVarRing a H1...
Qed.

Lemma nonzeroinv : forall a : F, a <> 0 -> / a <> 0.
Proof with try solve [ auto with field_hints | congruence ].
intros...
unfold not in |- *; intro...
assert (a * / a = 1)...
field...
assert (a * / a = a * 0)...
rewrite H1 in H2...
assert (a * 0 = 0)...
ring...
rewrite H3 in H2...
Qed.

Lemma opzero : forall a : F, a <> 0 -> - a <> 0.
Proof with try solve [ congruence ].
intros...
assert (a + - a = 0)...
apply Fplus_Fopp_r...
intuition...
rewrite H1 in H0...
assert (a = 0)...
assert (a + 0 = 0 + a)...
apply Fplus_sym...
rewrite H2 in H0...
assert (0 + a = a)...
apply Fplus_Ol...
Qed.

Theorem divnonzero: forall a b: F, a / b <> 0 -> a<>0.
  intros a b H1 H2; case H1; unfold Fdiv; rewrite H2; ring.
Qed.

Theorem multnonzero: forall a b: F, a*b<>0 -> a<>0 /\ b<>0.
  intros a b H1; split; intros H2; case H1; rewrite H2;ring.
Qed.

Theorem multnonzero_l: forall a b: F, a*b<>0 -> a<>0.
  intros a b H1; intros H2; case H1; rewrite H2;ring.
Qed.

Theorem multnonzero_r: forall a b: F, a*b<>0 -> b<>0.
  intros a b H1; intros H2; case H1; rewrite H2;ring.
Qed.

Lemma inverse_ratio : forall a b, a<>0 -> b<>0 -> a/b = 1 / (b/a).
Proof.
intros.
field; auto.
Qed.

Hint Resolve field_prop_1 field_prop_3 field_prop_4 field_prop_5 opzero
  nonzeromult nonzerodiv nonzeroinv inverse_ratio : field_hints.