proposition: Lemma lowDistApprox_repeat_sqrt_div2_left_total : forall (A : Set)(c : Comp A)(P : A -> bool) a, well_formed_comp c -> left_total (fun n => (lowDistApprox_repeat c P a (Nat.sqrt (Nat.div2 n)))).
proof: Proof. unfold left_total. intuition. edestruct lowDistApprox_repeat_left_total; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat