proposition: Lemma triangles_same_base : forall A B C D, Par A D B C -> signed_area A B C =F= signed_area D B C.
proof: Proof. intros A B C D. unfold signed_area. setoid_rewrite characterization_of_parallelism_F. decompose_coordinates;simpl. unfold cross_product;simpl. intros. spliter. nsatz. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems