proposition: Lemma ringF : (ring_theory OF OneF AddF MulF SubF OppF EqF).
proof: Proof. split; unfold OF, OneF, AddF, MulF, SubF, OppF, EqF, sig_rect; intro x; try intro y; try intro z. { destruct x as [x Hx]; simpl. elim (sum_f O x (col_trivial_3 O E) Hx). intros; simpl; apply sum_uniqueness with O E E' O x; try assumption. apply sum_O_B; auto using ncolOEE'. } { destruct x as [x Hx]; destruct y as [y Hy]; simpl. elim (sum_f x y Hx Hy). elim (sum_f y x Hy Hx). intros; simpl; apply sum_uniqueness with O E E' x y; try assumption. apply sum_comm; auto using ncolOEE'. } { destruct x as [x Hx]; destruct y as [y Hy]; destruct z as [z Hz]; simpl. destruct (sum_f y z Hy Hz) as [yPz HyPz]; simpl. destruct (sum_f x yPz Hx (sum_col y z yPz HyPz)) as [xPyPz HxPyPz]. destruct (sum_f x y Hx Hy) as [xPy HxPy]; simpl. destruct (sum_f xPy z (sum_col x y xPy HxPy) Hz) as [xPyPz' HxPyPz']; simpl. apply sum_uniqueness with O E E' x yPz; try assumption. apply (sum_assoc O E E' x y z xPy yPz xPyPz'); assumption. } { destruct x as [x Hx]; simpl. destruct (prod_f E x (col_trivial_2 O E) Hx) as [x' Hx']. simpl; apply prod_uniqueness with O E E' E x; try assumption. apply prod_1_l; auto using ncolOEE'. } { destruct x as [x Hx]; destruct y as [y Hy]; simpl. destruct (prod_f x y Hx Hy) as [xMy HxMy]. destruct (prod_f y x Hy Hx) as [yMx HyMx]; simpl. apply prod_uniqueness with O E E' x y; try assumption. apply prod_comm; auto using ncolOEE'. } { destruct x as [x Hx]; destruct y as [y Hy]; destruct z as [z Hz]; simpl. destruct (prod_f y z Hy Hz) as [yMz HyMz]; simpl. destruct (prod_f x yMz Hx (prod_col y z yMz HyMz)) as [xMyMz HxMyMz]. destruct (prod_f x y Hx Hy) as [xMy HxMy]; simpl. destruct (prod_f xMy z (prod_col x y xMy HxMy) Hz) as [xMyMz' HxMyMz']. simpl; apply prod_uniqueness with O E E' x yMz; try assumption. apply (prod_assoc O E E' x y z xMy yMz xMyMz');assumption. } { destruct x as [x Hx]; destruct y as [y Hy]; destruct z as [z Hz]; simpl. destruct (sum_f x y Hx Hy) as [xPy HxPy]; simpl. destruct (prod_f xPy z (sum_col x y xPy HxPy) Hz) as [xPyMz HxPyMz]. destruct (prod_f x z Hx Hz) as [xMz HxMz]; simpl. destruct (prod_f y z Hy Hz) as [yMz HyMz]; simpl. destruct (sum_f xMz yMz (prod_col x z xMz HxMz) (prod_col y z yMz HyMz)) as [xPyMz' HxPyMz']; simpl. apply sum_uniqueness with O E E' xMz yMz; try assumption. apply distr_r with x y z xPy; assumption. } { destruct x as [x Hx]; destruct y as [y Hy]; simpl. destruct (diff_f x y Hx Hy) as [xSy HxSy]. destruct (opp_f y Hy) as [Oy HOy]; simpl. destruct (sum_f x Oy Hx (opp_col y Oy HOy)) as [xSy' HxSy']; simpl. destruct HxSy as [Oy' [HOy' HxSy]]. assert (Oy = Oy') by ((apply opp_uniqueness with O E E' y);auto using ncolOEE'). subst; apply sum_uniqueness with O E E' x Oy';assumption. } { destruct x as [x Hx]; simpl. destruct (opp_f x Hx) as [Ox HOx]; simpl. destruct (sum_f x Ox Hx (opp_col x Ox HOx)) as [O' HO']; simpl. unfold Opp in HOx; apply sum_uniqueness with O E E' x Ox; try assumption. apply sum_comm; auto using ncolOEE'. } Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems