proposition: Lemma sesamath_4ieme_G2_ex44_1 : forall A B C D I J E F, Parallelogram_strict A B C D -> Midpoint I A D -> Midpoint J B C -> Bet A E C -> Bet I E B -> Bet A F C -> Bet D F J -> Parallelogram B J D I.
proof: Proof. intros. assert_diffs. assert_cols. assert_ncols. apply (Parallelogram_strict_Parallelogram A B C D) in H. assert(Par A D B C) by (apply(plg_par_2 A B C D);finish). assert(Cong A D B C) by (apply(plg_cong_2 A B C D);finish). assert(Cong D I B J) by (apply(cong_cong_half_2 A I D C J B);finish). assert(Par A D B J) by (apply(par_col_par A D B C);finish). assert(Par D I B J) by (apply(par_col_par_2 D A B J);finish). assert(exists M : Tpoint, Midpoint M A C /\ Midpoint M B D) by (apply(plg_mid A B C D);finish). destruct H31. spliter. assert(Par D C I x) by(apply(triangle_mid_par D C A x I);finish). assert(Par A B x J) by(apply(triangle_mid_par A B C J x);finish). assert(Par A B C D) by (apply(plg_par_1 A B C D);finish). assert(Par D C x J) by(apply(par_trans D C A B x J);finish). assert(Par x J I x) by(apply(par_trans x J D C I x);finish). assert(Col x J I) by (apply (par_id x J I);finish). show_distinct I J. { assert(~Par A D C B). (apply(inter_uniqueness_not_par A D C B I);finish). assert (Par A D C B);finish. } destruct (midpoint_existence A B) as [x0 Hx0]. destruct (midpoint_existence D C) as [x1 Hx1]. assert(Par A B J x /\ Cong A x0 J x) by(apply(triangle_mid_par_cong_1 C A B x0 J x);finish). assert(Par B A I x /\ Cong B x0 I x) by(apply(triangle_mid_par_cong_1 D B A x0 I x);finish). spliter. assert(Cong A x0 I x) by(apply(cong_transitivity A x0 x0 B I x);finish). assert( Cong I x J x) by(apply(cong_transitivity I x A x0 J x);finish). assert(Midpoint x I J) by(apply(l7_20_bis x I J);finish). apply (mid_plg B J D I x);finish. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter