proposition: Lemma prop_1_euclidean : forall A B, exists C, Cong A B A C /\ Cong A B B C.
proof: Proof. destruct exists_grid_spec as [SS [U1 [U2 Hgrid]]]. apply (exists_equilateral_triangle SS U1 U2 Hgrid). Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions