proposition: Lemma characterization_of_midpoint_F : forall A B I, Midpoint I A B <-> let (Ac, _) := coordinates_of_point_F A in let (Ax, Ay) := Ac in let (Bc, _) := coordinates_of_point_F B in let (Bx, By) := Bc in let (Ic, _) := coordinates_of_point_F I in let (Ix, Iy) := Ic in Ix * 2 - (Ax + Bx) =F= 0 /\ Iy * 2 - (Ay + By) =F= 0.
proof: Proof. intros; elim (eq_dec_points A B); intro HAB. { split; intro HMid; treat_equalities. { elim (coordinates_of_point_F I); intros Ic HIc. destruct Ic as [[Ix HIx] [Iy HIy]]; split; nsatz. } { cut (A = I); [intro; treat_equalities; Midpoint|]. rewrite characterization_of_equality_F; revert HMid. elim (coordinates_of_point_F A); intros Ac HAc. elim (coordinates_of_point_F I); intros Ic HIc. destruct Ac as [[Ax HAx] [Ay HAy]]. destruct Ic as [[Ix HIx] [Iy HIy]]. intro; spliter; split; assert (NU := neq20); nsatz. } } { split; intro HMid. { destruct HMid as [H HCong]. assert (HCol : Col A B I) by Col; clear H. revert HCol; revert HCong; revert HAB. rewrite characterization_of_neq_F, characterization_of_congruence_F, characterization_of_collinearity_F. elim (coordinates_of_point_F A); intros [Ax Ay] _. elim (coordinates_of_point_F B); intros [Bx By] _. elim (coordinates_of_point_F I); intros [Ix Iy] _. intros HAB HCong HCol. cut ((Ix * 2 - (Ax + Bx) =F= 0 /\ Iy * 2 - (Ay + By) =F= 0) \/ (Ax - Bx) * (Ax - Bx) + (Ay - By) * (Ay - By) =F= 0); [intuition|]. clear HAB; scnf; repeat rewrite <- mulF__eq0; try nsatz; rtauto. } { cut (Cong I A I B /\ Col A I B); [intros [HCong HCol]; induction (l7_20 I A B HCol HCong); intuition|]. clear HAB; rewrite characterization_of_congruence_F, characterization_of_collinearity_F. revert HMid. elim (coordinates_of_point_F A); intros [Ax Ay] _. elim (coordinates_of_point_F B); intros [Bx By] _. elim (coordinates_of_point_F I); intros [Ix Iy] _. intro; spliter; split; assert (NU := neq20); nsatz. } } Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems