proposition: Lemma supplement_AM_CongA : forall A B M C, Midpoint M A B -> AM_CongAL A M C B M C.
proof: Proof. intros A B M C. unfold AM_CongAL, twice_signed_area, Py, square_dist. rewrite characterization_of_midpoint_F. decompose_coordinates. unfold cross_product. simpl. intros;spliter. assert (NU : ~(2 * 2 =F= 0)) by prove_discr_for_powers_of_2. 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