proposition: Theorem root_max: forall p l, ulist l -> (forall i, In i p -> P i) -> (forall i, In i l -> P i) -> (forall x, In x l -> eval p x = zero) -> (length p <= length l)%nat -> forall x, P x -> eval p x = zero.
proof: Proof. intros p l; generalize p; elim l; clear l p; simpl; auto. intros p; case p; simpl; auto. intros a p1 _ _ _ _ H; contradict H; auto with arith. intros a p1 Rec p; case p. simpl; auto. intros a1 p2 H H1 H2 H3 H4 x px. assert (Hu: eval (a1 :: p2) a = zero); auto with datatypes. rewrite (div_correct_factor (a1 :: p2) a); auto with datatypes. match goal with |- mult ?X _ = _ => replace X with zero end; try apply mult_zero; auto. apply sym_equal; apply Rec; auto with datatypes. apply ulist_inv with (1 := H). intros i Hi; case (div_P (a1 :: p2) a); auto. intros x1 H5; case (mult_integral (eval (fst (div (a1 :: p2) a)) x1) (plus x1 (op a))); auto. apply eval_P; auto. intros i Hi; case (div_P (a1 :: p2) a); auto. rewrite <- div_correct_factor; auto. intros H6; case (ulist_app_inv _ (a::nil) p1 x1); simpl; auto. left. apply trans_equal with (plus zero x1); auto. rewrite <- (plus_op_zero a); try rewrite <- plus_assoc; auto. rewrite (fun x => plus_comm (op x)); try rewrite H6; try rewrite plus_comm; auto. apply sym_equal; apply plus_zero; auto. apply Nat.lt_succ_r;apply Nat.lt_le_trans with (length (a1 :: p2)); auto with zarith. apply length_decrease; auto with datatypes. Qed.
imports: ZArith List UList Tactic Permutation