proposition: Lemma lea_left_comm : forall A B C D E F, LeA A B C D E F -> LeA C B A D E F.
proof: Proof. intros. unfold LeA in *. ex_and H P. exists P. split. assumption. apply conga_left_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2