proposition: Lemma characterization_of_equality_F_aux : forall Ax Ay Bx By, Ax =F= Bx /\ Ay =F= By <-> (Ax - Bx) * (Ax - Bx) + (Ay - By) * (Ay - By) =F= OF.
proof: Proof. intros [Ax HAx] [Ay HAy] [Bx HBx] [By HBy]; unfold SubF, MulF, AddF, EqF; simpl. destruct (diff_f Ax Bx HAx HBx) as [AxMBx HAxMBx]; simpl. destruct (prod_f AxMBx AxMBx (diff_col Ax Bx AxMBx HAxMBx) (diff_col Ax Bx AxMBx HAxMBx)) as [ABx HABx]; simpl. destruct (diff_f Ay By HAy HBy) as [AyMBy HAyMBy]; simpl. destruct (prod_f AyMBy AyMBy (diff_col Ay By AyMBy HAyMBy) (diff_col Ay By AyMBy HAyMBy)) as [ABy HABy]; simpl. destruct (sum_f ABx ABy (prod_col AxMBx AxMBx ABx HABx) (prod_col AyMBy AyMBy ABy HABy)) as [s Hs]; simpl. split; intro H; [|apply eq_sym in H]; spliter; try split; treat_equalities. { apply sum_uniqueness with O E E' O O; [|apply sum_A_O; Col]. assert (AxMBx = O /\ AyMBy = O). { split; [apply diff_uniqueness with O E E' Ax Ax| apply diff_uniqueness with O E E' Ay Ay]; try apply diff_null; Col. apply ncolOEE'. apply ncolOEE'. } spliter; subst; assert (ABx = O /\ ABy = O); [|spliter; subst; assumption]. split; apply prod_uniqueness with O E E' O O; [|apply prod_0_l| |apply prod_0_l]; Col; auto using ncolOEE'. apply ncolOEE'. } { elim (eq_dec_points Ax Bx); intro Hx; [assumption|exfalso]. apply (O_not_positive O E); elim (eq_dec_points O AyMBy); intro Hy. { treat_equalities; apply prod_O_l_eq in HABy; subst. apply sum_A_O_eq in Hs; subst; try apply square_pos with E' AxMBx; Col. intro; treat_equalities; apply diff_null_eq in HAxMBx; intuition. apply ncolOEE'. } { apply sum_pos_pos with E' ABx ABy; [apply square_pos with E' AxMBx|apply square_pos with E' AyMBy|assumption]; try assumption; intro; treat_equalities; apply diff_null_eq in HAxMBx; intuition. } } { subst; elim (eq_dec_points Ay By); intro Hy; [assumption|exfalso]. apply (O_not_positive O E); elim (eq_dec_points O AxMBx); intro Hx. { treat_equalities; apply prod_O_l_eq in HABx; subst. apply sum_O_B_eq in Hs; subst; try apply square_pos with E' AyMBy; Col. intro; treat_equalities; apply diff_null_eq in HAyMBy; intuition. apply ncolOEE'. } { apply sum_pos_pos with E' ABx ABy; [apply square_pos with E' AxMBx|apply square_pos with E' AyMBy|assumption]; try assumption; intro; treat_equalities; apply diff_null_eq in HAyMBy; intuition. } } Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems