proposition: Lemma l7_22 : forall A1 A2 B1 B2 C M1 M2, Bet A1 C A2 -> Bet B1 C B2 -> Cong C A1 C B1 -> Cong C A2 C B2 -> Midpoint M1 A1 B1 -> Midpoint M2 A2 B2 -> Bet M1 C M2.
proof: Proof. intros. assert (Le C A1 C A2 \/ Le C A2 C A1). eapply le_cases. induction H5. eapply l7_22_aux. apply H. apply H0. apply H1. apply H2. assumption. assumption. assumption. apply between_symmetry. eapply l7_22_aux with A2 A1 B2 B1; finish. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR