proposition: Lemma conga_left_comm : forall A B C D E F, CongA A B C D E F -> CongA C B A D E F.
proof: Proof. intros. apply conga_sym, conga_right_comm, conga_sym. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2