proposition: Lemma put_neg_in_goal : forall A B, A \/ B -> (~ A -> B).
proof: Proof. tauto. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems