proposition: Lemma characterization_of_betweenness_F : forall A B C, Bet A B C <-> 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 (Cc, _) := coordinates_of_point_F C in let (Cx, Cy) := Cc in exists T, 0 <= T /\ T <= 1 /\ T * (Cx - Ax) =F= Bx - Ax /\ T * (Cy - Ay) =F= By - Ay.
proof: Proof. intros. elim (coordinates_of_point_F A); intros Ac HAc. elim (coordinates_of_point_F B); intros Bc HBc. elim (coordinates_of_point_F C); intros Cc HCc. destruct Ac as [[Ax HAx] [Ay HAy]]. destruct Bc as [[Bx HBx] [By HBy]]. destruct Cc as [[Cx HCx] [Cy HCy]]. unfold MulF, SubF, EqF, LeF; simpl. destruct (diff_f Bx Ax HBx HAx) as [BxMAx HBxMAx]; simpl. destruct (diff_f By Ay HBy HAy) as [ByMAy HByMAy]; simpl. destruct (diff_f Cx Ax HCx HAx) as [CxMAx HCxMAx]; simpl. destruct (diff_f Cy Ay HCy HAy) as [CyMAy HCyMAy]; simpl. split; intro HBet; [|destruct HBet as [T HBet]]. { apply -> (characterization_of_betweenness O E E' SS U1 U2 A Ax Ay B Bx By C Cx Cy BxMAx ByMAy CxMAx CyMAy) in HBet; auto; destruct HBet as [T [H [HCol [HGe0 [HLe1 [HTx HTy]]]]]]; clear H. exists (exist (fun P => Col O E P) T HCol); simpl; do 2 (split; auto). destruct (prod_f T CxMAx HCol (diff_col Cx Ax CxMAx HCxMAx)) as [Tx HTx']. destruct (prod_f T CyMAy HCol (diff_col Cy Ay CyMAy HCyMAy)) as [Ty HTy']; simpl. split; [apply prod_uniqueness with O E E' T CxMAx| apply prod_uniqueness with O E E' T CyMAy]; assumption. } { destruct (prod_f (proj1_sig T) CxMAx (proj2_sig T) (diff_col Cx Ax CxMAx HCxMAx)) as [Tx HTx']. destruct (prod_f (proj1_sig T) CyMAy (proj2_sig T) (diff_col Cy Ay CyMAy HCyMAy)) as [Ty HTy']. simpl in *; destruct HBet as [HGe0 [HLe1 [HTx HTy]]]; treat_equalities. apply <- (characterization_of_betweenness O E E' SS U1 U2 A Ax Ay B Bx By C Cx Cy Tx Ty CxMAx CyMAy); auto. exists (proj1_sig T); repeat (split; auto); [assert (TT:=ncolOEE');assert_diffs; auto|]. apply (proj2_sig T). } Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems