proposition: Lemma exists_equilateral_triangle : forall A B, exists C, Cong A B A C /\ Cong A B B C.
proof: Proof. intros. destruct (exists_cong_per A B A B) as [P HP]. destruct (exists_cong_per A P A B) as [Q HQ]. destruct (midpoint_existence A Q) as [R HR]. destruct (midpoint_existence A B) as [I HI]. destruct (exists_cong_per A I A R) as [C HC]. exists C. spliter. revert dependent A . intro A. convert_to_algebra. decompose_coordinates; intros; spliter; split; assert (NU : ~(2 * 2 =F= 0)) by prove_discr_for_powers_of_2; assert (NUm : ~(-(2 * 2) =F= 0)) by prove_discr_for_powers_of_2; assert (NUm' : ~(-(2 * (2 * 2)) =F= 0)) by prove_discr_for_powers_of_2; 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