proposition: Lemma distr_l : forall O E E' A B C D AB AC AD, Sum O E E' B C D -> Prod O E E' A B AB -> Prod O E E' A C AC -> (Prod O E E' A D AD -> Sum O E E' AB AC AD).
proof: Proof. intros. assert(HS:=H). unfold Sum in H. spliter. ex_and H3 B'. ex_and H4 C1. assert(HP1:=H0). assert(HP2:=H1). assert(HPS:=H2). unfold Prod in H0. spliter. ex_and H8 B''. assert(~Col O E E' /\ Col O E A /\ Col O E B /\ Col O E C /\ Col O E D). unfold Ar2 in *. spliter. repeat split; Col. spliter. assert(HH:=grid_not_par O E E' H11). spliter. assert(B' = B''). apply(pj_uniqueness O E E' B); Col. subst B''. unfold Prod in H1. spliter. ex_and H22 C'. unfold Prod in H2. spliter. ex_and H25 D'. assert(Sum O E' E B' C' D'). apply(proj_preserves_sum O E E' B C D B' C' D'); auto. repeat split; Col. induction(eq_dec_points A O). subst A. assert(HH1:= prod_0_l O E E' B H11 H13). assert( AB = O). apply (prod_uniqueness O E E' O B); auto. subst AB. assert(HH2:= prod_0_l O E E' C H11 H14). assert( AC = O). apply (prod_uniqueness O E E' O C); auto. subst AC. assert(HH3:= prod_0_l O E E' D H11 H15). assert( AD = O). apply (prod_uniqueness O E E' O D); auto. subst AD. apply sum_O_O; Col. assert(Sum O E' A B' C' D'). apply(sum_y_axis_change O E' E A B' C' D'); auto. intro. apply H11. ColR. assert(Sum O A E' AB AC AD). unfold Ar2 in *. spliter. apply(proj_preserves_sum O E' A B' C' D' AB AC AD); auto. repeat split; auto. ColR. ColR. ColR. apply(sum_x_axis_unit_change O A E' E AB AC AD); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum