proposition: Lemma tight_apart_cpoly_ap : tight_apart cpoly_eq cpoly_ap.
proof: Proof. red in |- *. intros x y. pattern x, y in |- *. apply cpoly_double_ind0'. simple induction p. simpl in |- *. unfold iff in |- *. unfold Not in |- *. split. auto. intros H H0; inversion H0. simpl in |- *. intros s c H. cut (Not (s [#] [0]) <-> s [=] [0]). unfold Not in |- *. intro H0. elim H0; intros H1 H2. split. intro H3. split; auto. elim H; intros H4 H5. apply H4. intro H6. auto. intros H3 H4. elim H3; intros H5 H6. elim H4; intros H7. auto. elim H; intros H8 H9. unfold Not in H8. elim H9; assumption. apply (ap_tight CR). simple induction p. simpl in |- *. intro c. cut (Not (c [#] [0]) <-> c [=] [0]). unfold Not in |- *. intro H. elim H; intros H0 H1. split. auto. intros H2 H3. elim H3; intro H4. tauto. elim H4. apply (ap_tight CR). simpl in |- *. intros s c H d. generalize (H d). generalize (ap_tight CR d [0]). generalize (ap_tight CR s [0]). unfold Not in |- *. intros H0 H1 H2. elim H0; clear H0; intros H3 H4. elim H1; clear H1; intros H0 H5. elim H2; clear H2; intros H1 H6. tauto. simpl in |- *. unfold Not in |- *. intros p q c d H. elim H; intros H0 H1. split. intro H2. split. generalize (ap_tight CR c d). unfold Not in |- *; tauto. tauto. intros H2 H3. elim H3. elim H2. intros H4 H5 H6. generalize (ap_tight CR c d). unfold Not in |- *. tauto. elim H2. auto. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational