proposition: Lemma conga_pseudo_refl : forall A B C, A <> B -> C <> B -> CongA A B C C B A.
proof: Proof. intros. unfold CongA. repeat split; try assumption. prolong B A A' B C. prolong B C C' B A. prolong B A A'' B C. prolong B C C'' B A. exists A', C', C'', A''. repeat split; try assumption. assert (A' = A'') by (pose (construction_uniqueness B A); eauto). subst A''. assert (C' = C'') by (pose (construction_uniqueness B C); eauto). subst C''. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2