proposition: Lemma fieldF : field_theory OF OneF AddF MulF SubF OppF DivF InvF EqF.
proof: Proof. split; unfold OF, OneF, MulF, DivF, InvF, EqF, sig_rect; simpl; [apply ringF|assert (T:=ncolOEE');assert_diffs; auto|intros p q|intros p Hp]. { destruct (div_f (proj1_sig p) (proj1_sig q) (proj2_sig p) (proj2_sig q)) as [pDq HpDq]; simpl. destruct (inv_f (proj1_sig q)(proj2_sig q)) as [Iq HIq]; simpl. destruct (prod_f (proj1_sig p) Iq (proj2_sig p) (inv_col (proj1_sig q) Iq HIq)) as [pDq' HpDq']. simpl; destruct HpDq as [Iq' [HIq' HpDq]]. assert (Iq = Iq'); [apply inv_uniqueness with (proj1_sig q)| subst; apply prod_uniqueness with O E E' (proj1_sig p) Iq']; assumption. } { destruct (inv_f (proj1_sig p) (proj2_sig p)) as [Ip HIp]; simpl. destruct (prod_f Ip (proj1_sig p) (inv_col (proj1_sig p) Ip HIp) (proj2_sig p)) as [E'' HE'']. simpl; elim HIp; clear HIp; intro HIp; [|spliter; treat_equalities; intuition]. destruct HIp as [H HIp]; clear H. apply prod_uniqueness with O E E' Ip (proj1_sig p); assumption. } Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems