proposition: Lemma plgf_not_comm : forall A B C D, A <> B -> Parallelogram_flat A B C D -> ~ Parallelogram_flat A B D C /\ ~ Parallelogram_flat B A C D.
proof: Proof. intros. assert(HH0:=plgf_mid A B C D H0). split. intro. assert(HH1:=plgf_mid A B D C H1). unfold Parallelogram_flat in *. spliter. ex_and HH0 M. assert(A = B /\ C = D \/ A = D /\ C = B). apply(midpoint_cong_uniqueness A C B D M). Col. split; assumption. Cong. induction H12. spliter. contradiction. spliter. subst D. subst C. induction H5; tauto. ex_and HH0 M. unfold Parallelogram_flat in *. intro. spliter. assert(A = B /\ C = D \/ A = D /\ C = B). apply(midpoint_cong_uniqueness A C B D M). Col. split; assumption. Cong. induction H12. spliter. contradiction. spliter. subst D. subst C. induction H7; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel