proposition: Lemma parallelogram_strict_midpoint : forall A B C D I, Parallelogram_strict A B C D -> Col I A C -> Col I B D -> Midpoint I A C /\ Midpoint I B D.
proof: Proof. intros. assert (T:=Parallelogram_strict_Parallelogram A B C D H). assert (HpF := plg_mid A B C D T). elim HpF; intros I' HI;spliter;clear HpF. assert (H01 : Col A C I). Col. assert (H02 : Col D B I). Col. assert (H03 : ~Col A D C). apply parallelogram_strict_not_col_3 in H. Col. unfold Parallelogram_strict in H. decompose [and] H. assert (H8 := two_sides_not_col A C B D H4). assert (MDB:D<>B). assert (Col A I' C). assert (H9 := midpoint_bet A I' C H2). assert (H10 := bet_col A I' C H9). assumption. assert (H11 : ~ Col A C D). Col. assert (H12 := l7_2 I' B D H3). assert (H13 : Col A C I'). Col. apply (midpoint_distinct A C I' D B H11 H13 H12). assert (H11 : Col D B I'). assert (H14 := midpoint_bet B I' D H3). assert (H15 := bet_col B I' D H14). Col. assert (H12 : Col A C I'). assert (H14 := midpoint_bet A I' C H2). assert (H15 := bet_col A I' C H14). Col. apply not_col_permutation_5 in H03. assert (H13 := l6_21 A C D B I I' H03 MDB H01 H12 H02 H11). split. rewrite H13;assumption. subst;assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates