proposition: Theorem all_0_shrink_0 : ∀ la cnt k, (∀ n, (List.nth n la 0 = 0)%K) → (∀ n, (List.nth n (list_shrink_aux cnt k la) 0 = 0)%K).
proof: Proof. intros la cnt k H n. revert cnt k n. induction la as [| a]; intros; [ destruct n; reflexivity | simpl ]. destruct cnt; simpl. destruct n; simpl. pose proof (H O); assumption. apply IHla; clear n; intros n. pose proof (H (S n)); assumption. apply IHla; clear n; intros n. pose proof (H (S n)); assumption. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn