proposition: Lemma prop_26_1 : forall A B C D E F, ~ Col A B C -> CongA B A C E D F -> CongA A B C D E F -> Cong A B D E -> Cong A C D F /\ Cong B C E F /\ CongA A C B D F E.
proof: Proof. apply l11_50_1. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions