proposition: Lemma conga_distinct : forall A B C D E F, CongA A B C D E F -> CongA A B C D E F /\ A <> B /\ C <> B /\ D <> E /\ F <> E.
proof: Proof. intros. split. assumption. unfold CongA in H. spliter. repeat split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2