proposition: Lemma retract_zero_wretract : forall f n, retract f n -> (forall k, (n <= k)%nat -> f k == 0) -> wretract f.
proof: Proof. red; intros. assert (k < n \/ n <= k)%nat; intuition. lia. rewrite H0; auto. Qed.
imports: ALEA(Utheory)