proposition: Lemma sesamath_4ieme_G2_ex35 : forall G A Z F E R, ~ Col G A Z -> Per G A Z -> Midpoint F A Z -> Midpoint E G Z -> Midpoint R G A -> Rectangle F E R A.
proof: Proof. intros G A Z F E R HnCol HPER HM1 HM2 HM3. assert_diffs. assert_cols. assert (Par A Z E R) by (perm_apply (triangle_mid_par Z A G R E)). assert (Par A G F E) by perm_apply (triangle_mid_par A G Z E F). assert (Par A F E R) by (apply par_col_par_2 with Z;finish). assert (Par A R E F) by (apply par_col_par_2 with G;finish). assert (~Col A R F) by (intro;apply HnCol;ColR). assert (Par_strict A R E F) by (apply par_not_col_strict with F;finish). assert (Plg F E R A) by (apply pars_par_plg;finish). assert (Per F A R) by (apply col_col_per_per with Z G;finish). apply (plg_per_rect);auto. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter