proposition: Lemma conga__lea : forall A B C D E F, CongA A B C D E F -> LeA A B C D E F.
proof: Proof. intros. unfold LeA. exists F. split. apply inangle3123. apply (conga_diff45 A B C D E F); assumption. apply (conga_diff56 A B C D); assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2