proposition: Lemma conga_trivial_1 : forall A B C D, A<>B -> C<>D -> CongA A B A C D C.
proof: Proof. intros. unfold CongA. repeat split; try assumption. prolong B A A' D C. prolong D C C' B A. exists A', A', C', C'. repeat split;Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2