proposition: Lemma conga_refl : forall A B C, A <> B -> C <> B -> CongA A B C A B C.
proof: Proof. intros. apply l11_3_bis. exists A. exists C. exists A. exists C. repeat split; Between; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2