proposition: Lemma signed_area_AAB : forall A B, signed_area A A B =F= 0.
proof: Proof. intros. unfold signed_area, cross_product. decompose_coordinates;simpl. field. prove_discr_for_powers_of_2. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems