proposition: Lemma plgf3_mid : forall A B C, Parallelogram_flat A B A C -> Midpoint A B C.
proof: Proof. intros. unfold Parallelogram_flat in H. spliter. assert(B=C \/ Midpoint A B C). eapply l7_20. Col. Cong. induction H3. tauto. induction H4. contradiction. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel