proposition: Lemma plgf_trivial_neq : forall A C D, Parallelogram_flat A A C D -> C = D /\ A <> C.
proof: Proof. intros. unfold Parallelogram_flat in H. spliter. apply cong_symmetry in H1. apply cong_identity in H1. subst D. split. reflexivity. induction H3; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel