proposition: Lemma neg_and_eqF : forall A B C D, ~ (EqF A B /\ EqF C D) <-> ~ EqF A B \/ ~ EqF C D.
proof: Proof. intros A B C D; split; intro H; induction (eq_dec_F A B); induction (eq_dec_F C D); intuition. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems