proposition: Lemma mid_plg : forall A B C D M, (A <> C \/ B <> D ) -> Midpoint M A C -> Midpoint M B D -> Parallelogram A B C D.
proof: Proof. intros. unfold Parallelogram. induction(col_dec A B C). right. apply (mid_plgf _ _ _ _ M); assumption. left. apply (mid_plgs _ _ _ _ M); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel