proposition: Lemma signed_area_sum : forall A B C D, signed_area A B C =F= signed_area A B D + signed_area A D C + signed_area D B C.
proof: Proof. intros. unfold signed_area. decompose_coordinates. unfold cross_product;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