proposition: Lemma per_mid_per : forall A B X Y M, A <> B -> Per X A B -> Midpoint M A B -> Midpoint M X Y -> Cong A X B Y /\ Per Y B A.
proof: Proof. intros. assert (Cong A X B Y). eapply l7_13. apply l7_2. apply H1. apply l7_2. assumption. split. assumption. unfold Per in H0. ex_and H0 B'. double A B A'. assert (Cong B X A Y). eapply l7_13. apply H1. apply l7_2. assumption. assert (OFSC B A B' X A B A' Y). unfold OFSC. repeat split. apply midpoint_bet. assumption. apply midpoint_bet. assumption. apply cong_pseudo_reflexivity. unfold Midpoint in *. spliter. eapply cong_transitivity. apply cong_symmetry. apply H8. apply cong_left_commutativity. assumption. assumption. assumption. unfold Per. exists A'. split. assumption. assert (Cong B' X A' Y). eapply five_segment_with_def. apply H7. intro. apply H. subst B. reflexivity. eapply cong_transitivity. apply cong_commutativity. apply cong_symmetry. apply H6. eapply cong_transitivity. apply H4. apply cong_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar