proposition: Lemma sesamath_4ieme_G2_ex36 : forall A B C H I J, isosceles B A C -> Perp A H B C -> Col B H C -> Midpoint I A B -> Midpoint J A C -> Rhombus A I H J.
proof: Proof. intros. assert_diffs. assert_cols. assert (~ Col B A C /\ B <> H /\ C <> H /\ Midpoint H B C /\ CongA H A B H A C) by (apply (isosceles_foot__midpoint_conga B A C );finish). spliter. assert (Plg A I H J). { assert (Plg J H I A). apply (sesamath_4ieme_G2_ex36_aux C A B J H I);finish. apply parallelogram_to_plg. apply plg_to_parallelogram in H14. apply Plg_perm in H14. spliter;auto. } assert (Par I J B C) by (perm_apply (triangle_mid_par B C A J I)). assert (Perp A H I J) by (perm_apply (cop_par_perp__perp B C I J A H)). apply perp_rmb;finish. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter