proposition: Lemma sesamath_4ieme_G2_ex42 : forall A B C I K L J G, ~Col A B C -> is_gravity_center G A B C -> Midpoint I A C -> Midpoint J A B -> Midpoint K B G -> Midpoint L C G -> Parallelogram I J K L.
proof: Proof. intros. assert_diffs. assert_cols. assert (G<>A) by (apply(is_gravity_center_diff_1 A B C G);finish). assert (Par B C K L) by(apply(triangle_mid_par B C G L K);finish). assert (G<>C) by (apply(is_gravity_center_diff_3 A B C G);finish). assert_diffs. assert (Midpoint J B A) by(apply(l7_2 J A B);finish). assert(is_gravity_center G C B A) by(apply(is_gravity_center_perm_5 A B C G);finish). assert(Midpoint G J L) by(apply(is_gravity_center_third C B A G L J);finish). assert_diffs. assert(Parallelogram I L K J) by(apply(varignon.varignon_aux_aux A C G B I L K J);finish). apply(Plg_perm I L K J);finish. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter