proposition: Lemma parallelogram__coplanar : forall A B C D, Parallelogram A B C D -> Coplanar A B C D.
proof: Proof. intros A B C D [Hs|Hf]. apply plgs__coplanar, Hs. apply plgf__coplanar, Hf. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality