proposition: Lemma change_grid_prod_l_O : forall O E E' B C O' A' B' C', Par_strict O E O' E' -> Ar1 O E O B C -> Ar1 O' E' A' B' C' -> Pj O O' E E' -> Pj O O' O A' -> Pj O O' B B' -> Pj O O' C C' -> Prod O E E' O B C -> Prod O' E' E A' B' C'.
proof: Proof. intros. assert(HP:= H6). unfold Prod in H6. spliter. unfold Ar2 in H6. clear H7. spliter. assert(C = O). apply prod_O_l_eq in HP. assumption. subst C. assert(Par O O' O A'). induction H3. Par. subst A'. unfold Ar1 in H1. spliter. apply False_ind. apply H. exists O. split; Col. induction H10. apply False_ind. apply H10. exists O. split; Col. spliter. assert(A' = O'). apply (l6_21 O O' E' O'); Col. intro. apply H. exists O. split; Col. unfold Ar1 in H1. spliter. auto. unfold Ar1 in H1. spliter. Col. subst A'. clean_trivial_hyps. assert(Par O O' O C'). induction H5. Par. subst C'. apply False_ind. unfold Ar1 in H1. spliter. apply H. exists O. split; Col. induction H7. apply False_ind. apply H7. exists O. split; Col. spliter. assert(C' = O'). apply (l6_21 O O' E' O'); Col. intro. apply H. exists O. split; Col. unfold Ar1 in H1. spliter. auto. unfold Ar1 in H1. spliter. Col. subst C'. apply(prod_0_l). intro. apply H. exists E. split; Col. unfold Ar1 in H1. spliter. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum