proposition: Lemma lowDistApprox_repeat_sqrt_le : forall n (A : Set)(c : Comp A)(P : A -> bool) a v1 v2, well_formed_comp c -> (exists a, In a (filter P (getSupport c))) -> lowDistApprox (Repeat c P) a n v1 -> lowDistApprox_repeat c P a (Nat.sqrt (Nat.div2 n)) v2 -> n > 1 -> v2 <= v1.
proof: Proof. intuition. edestruct (dat_exists_repeat2). eauto. rewrite repeat_low_tree_approx_same_inv; eauto. destruct H0. edestruct dat_exists. eapply well_formed_Repeat. eapply comp_eq_dec; eauto. eauto. eauto. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply low_tree_approx_same_inv. eapply H0. eapply H1. } eapply lowDistApprox_dat_better_le. eapply dat_correct_repeat_same in H0. eapply dat_better_repeat_sqrt; eauto. eauto. econstructor; eauto. destruct n. lia. destruct n. lia. simpl. eapply Nat.lt_le_trans. econstructor. eapply Nat.le_trans. rewrite <- Nat.sqrt_1. eauto. eapply Nat.sqrt_le_mono. lia. Unshelve. eapply comp_eq_dec; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat