proposition: Lemma mid_preserves_col : forall A B C M A' B' C', Col A B C -> Midpoint M A A' -> Midpoint M B B' -> Midpoint M C C' -> Col A' B' C'.
proof: Proof. intros. induction H. assert (Bet A' B' C'). eapply l7_15 with A B C M;auto. Col. induction H. assert (Bet B' C' A'). eapply l7_15 with B C A M;auto. Col. assert (Bet C' A' B'). eapply l7_15 with C A B M;auto. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar