proposition: Lemma lem14 : forall (s1 s2 : seq K) (P1 : fresh_seq K s1) (P2 : fresh_seq K s2), (permutation K s1 s2) -> dd K f s1 P1 [=] dd K f s2 P2.
proof: Proof. intros s1 s2 P1 P2 perm. induction perm. algebra. algebra. assert (fresh_seq K (a :: s1)). apply fresh_cons. inversion P1. inversion H1. inversion X. unfold sqfresh. apply insq. exact X1. inversion P1. inversion H2. exact H6. assert (fresh_seq K (b :: s1)). inversion P1. exact H3. inversion P1. inversion H3. inversion X. assert (a [-] b [#] Zero). apply minus_ap_zero. apply ap_symmetric. exact X0. rewrite (dd_reduce K f s1 a b P1 H H0 X2). assert (fresh_seq K (a :: s2)). apply fresh_cons. inversion P2. inversion H7. inversion X3. apply insq. exact X5. inversion P2. inversion H8. exact H12. assert (fresh_seq K (b :: s2)). inversion P2. exact H9. rewrite (dd_reduce K f s2 a b P2 H5 H6 X2). apply div_wd. rewrite (IHperm2 H H5). rewrite (IHperm3 H0 H6). reflexivity. reflexivity. assert (fresh_seq K (a :: s)). inversion P2. exact H2. assert (fresh_seq K (b :: s)). inversion P1. exact H3. inversion P1. inversion H3. inversion X. assert (a [-] b [#] Zero). apply minus_ap_zero. apply ap_symmetric. exact X0. rewrite (dd_reduce K f s a b P1 H H0 X2). assert (b [-] a [#] Zero). apply minus_ap_zero. exact X0. rewrite (dd_reduce K f s b a P2 H0 H X3). apply eq_div. rewrite ring_dist_minus. rewrite ring_dist_minus. rewrite dist_2b. rewrite dist_2b. rewrite dist_2b. rewrite dist_2b. set (cr_mult (dd K f (a :: s) H) b). set (cr_mult (dd K f (b :: s) H0) b). set (cr_mult (dd K f (a :: s) H) a). set (cr_mult (dd K f (b :: s) H0) a). rewrite assoc_1. rewrite assoc_1. rewrite <- minus_plus. rewrite <- minus_plus. rewrite (cag_commutes_unfolded K s3 s2). rewrite (cag_commutes_unfolded K _ s1). rewrite assoc_2. rewrite (cag_commutes_unfolded K _ s4). rewrite assoc_2. rewrite cg_minus_unfolded. rewrite cg_minus_unfolded. rewrite (cag_commutes_unfolded K s1 s4). reflexivity. assert (fresh_seq K s2). apply (perm_fresh s1). exact P1. exact perm1. rewrite (IHperm1 P1 H). rewrite (IHperm2 H P2). reflexivity. Qed.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass