proposition: Lemma lea_out_lea : forall A B C D E F A' C' D' F', Out B A A' -> Out B C C' -> Out E D D' -> Out E F F' -> LeA A B C D E F -> LeA A' B C' D' E F'.
proof: Proof. intros. unfold LeA in *. ex_and H3 P. exists P. split. apply (l11_25 P D E F D' F' P); try apply l6_6; auto. apply out_trivial. unfold CongA in H4. tauto. apply (l11_10 A B C D E P); try apply l6_6; auto. apply out_trivial. unfold CongA in H4. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order