proposition: Lemma l11_18_1 : forall A B C D, Bet C B D -> B <> C -> B <> D -> A <> B -> Per A B C -> CongA A B C A B D.
proof: Proof. intros. spliter. assert (Per A B D). eapply per_col. apply H0. assumption. unfold Col. right; right. apply between_symmetry. assumption. apply l11_16; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2