proposition: Lemma plg_irreflexive : forall A B, ~ Parallelogram A B A B.
proof: Proof. intros. intro. induction H. apply plgs_irreflexive in H. assumption. apply plgf_irreflexive in H. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel