proposition: Lemma l11_36 : forall A B C D E F A' D', A <> B -> A' <> B -> D <> E -> D' <> E -> Bet A B A' -> Bet D E D' -> (LeA A B C D E F <-> LeA D' E F A' B C).
proof: Proof. intros. split. intro. assert(HH:=H5). apply l11_29_a in H5. unfold LeA. ex_and H5 P. exists P. split. eapply (in_angle_reverse A); try assumption. eapply l11_13. apply conga_sym. apply H6. assumption. assumption. assumption. assumption. intro. assert(HH:=H5). unfold LeA in H5. apply l11_29_b. ex_and H5 P. exists P. split. eapply (in_angle_reverse A'); try assumption. apply between_symmetry. assumption. eapply l11_13. apply conga_sym. apply H6. apply between_symmetry. assumption. assumption. apply between_symmetry. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2