proposition: Lemma characterization_of_right_triangle_F : forall A B C, Per 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 (Ax - Bx) * (Bx - Cx) + (Ay - By) * (By - Cy) =F= 0.
proof: Proof. intros; unfold Per. destruct (symmetric_point_construction C B) as [D HM]; revert HM. setoid_rewrite characterization_of_congruence_F. setoid_rewrite characterization_of_midpoint_F. elim (coordinates_of_point_F A); intros [Ax Ay] _. elim (coordinates_of_point_F B); intros [Bx By] _. elim (coordinates_of_point_F C); intros [Cx Cy] _; intro H. split; [clear H; clear D; intro H; destruct H as [D [H1 H2]]; revert H2; revert H1| intro H1; exists D; split; [assumption|revert H1; revert H]]; elim (coordinates_of_point_F D); intros Dc _; destruct Dc as [Dx Dy]; intros; spliter; assert (NU := neqO_mul_neqO _ _ neq20 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