proposition: Lemma lea_out4__lea : forall A B C D E F A' C' D' F', LeA A B C D E F -> Out B A A' -> Out B C C' -> Out E D D' -> Out E F F' -> LeA A' B C' D' E F'.
proof: Proof. intros A B C D E F A' C' D' F' Hl HA HC HD HF. apply (l11_30 A B C D E F); trivial; apply out2__conga; apply l6_6; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2