proposition: Lemma retractS_intro: forall (f : nat -> U) (n : nat), retract f n -> f n <= [1-] (sigma f n) -> retract f (S n).
proof: Proof. unfold retract; intros. assert ((k<n)%nat \/ k=n); try lia; intuition; subst; auto. Qed.
imports: ALEA(Utheory)