proposition: Lemma change_grid_prod1 : forall O E E' B C O' A' B' C', Par_strict O E O' E' -> Ar1 O E E B C -> Ar1 O' E' A' B' C' -> Pj O O' E E' -> Pj O O' E A' -> Pj O O' B B' -> Pj O O' C C' -> Prod O E E' E B C -> Prod O' E' E A' B' C'.
proof: Proof. intros. induction (eq_dec_points B O). subst B. apply prod_comm. unfold Ar1 in *. spliter. apply(change_grid_prod_l_O O E E' E C O' B' A' C'); auto. repeat split; Col. repeat split; Col. apply prod_comm. assumption. induction(eq_dec_points C O). subst C. apply prod_null in H6. induction H6. subst E. apply par_strict_distinct in H. tauto. subst B. tauto. assert(HP:= H6). unfold Prod in H6. spliter. unfold Ar2 in H6. spliter. clear H9. unfold Ar1 in H1. spliter. assert(HH:=prod_1_l O E E' B H6 H11). assert(B = C). apply (prod_uniqueness O E E' E B); auto. subst C. assert(A' = E'). apply(l6_21 E E' O' E'); Col. intro. apply H. exists E. split; Col. induction H2; induction H3. assert(Par E A' E E'). apply(par_trans _ _ O O'); Par. induction H15. apply False_ind. apply H15. exists E. split; Col. spliter. Col. subst A'. Col. subst E'. Col. subst A'. Col. subst A'. assert(C' = B'). apply(l6_21 B' B O' E'); Col. intro. apply H. exists B. split; Col. assert(B' <> O'). intro. subst B'. induction H4. induction H4. apply H4. exists O'. split; Col. spliter. apply H. exists O'. split; Col. ColR. subst B. apply H. exists O'. split; Col. ColR. induction H4; induction H5. assert(Par B C' B B'). apply(par_trans _ _ O O'); Par. induction H15. apply False_ind. apply H15. exists B. split; Col. spliter. Col. subst C'. Col. subst B'. Col. subst C'. Col. subst C'. apply (prod_1_l O' E' E); Col. intro. apply H. exists E. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum