proposition: Lemma Per_mid_rectangle : forall A B C I J K, A <> B -> B <> C -> Per B A C -> Midpoint I B C -> Midpoint J A C -> Midpoint K A B -> Rectangle A J I K.
proof: Proof. intros. assert_diffs. assert_cols. elim (eq_dec_points A C); intro; apply plg_per_rect. treat_equalities. assert (HM : exists M : Tpoint, Midpoint M J I) by (apply midpoint_existence); decompose [ex] HM; repeat split; intuition; exists x; intuition. treat_equalities; intuition. assert( Par A B J I /\ Par A C I K /\ Par B C J K /\ Cong A K I J /\ Cong B K I J /\ Cong A J I K /\ Cong C J I K /\ Cong B I J K /\ Cong C I J K) by (apply triangle_mid_par_cong; intuition). spliter. elim (col_dec A B C); intro; assert_diffs. apply parallelogram_to_plg; unfold Parallelogram; right; unfold Parallelogram_flat; repeat split. ColR. ColR. assumption. assumption. right; intro; subst; assert (B = C) by (apply symmetric_point_uniqueness with A K; assumption); contradiction. apply pars_par_plg. assert (Par_strict A B J I /\ Par_strict A C I K /\ Par_strict B C J K /\ Cong A K I J /\ Cong B K I J /\ Cong A J I K /\ Cong C J I K /\ Cong B I J K /\ Cong C I J K) by (apply triangle_mid_par_strict_cong; intuition). spliter. apply par_strict_symmetry; apply par_strict_col_par_strict with C; intuition; apply par_strict_symmetry; apply par_strict_right_comm; assumption; Col. Par. Col. assert (Par_strict A B J I /\ Par_strict A C I K /\ Par_strict B C J K /\ Cong A K I J /\ Cong B K I J /\ Cong A J I K /\ Cong C J I K /\ Cong B I J K /\ Cong C I J K) by (apply triangle_mid_par_strict_cong; intuition). spliter. apply par_symmetry; apply par_col_par with B; intuition; apply par_symmetry; apply par_strict_par; assumption. left; apply l8_3 with B; try apply l8_2; try apply l8_3 with C; try apply l8_2; try assumption; intuition; Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon