proposition: Lemma lowDistApprox_le_1 : forall (A : Set)(c : Comp A) a n r, lowDistApprox c a n r -> r <= 1.
proof: Proof. intuition. unfold lowDistApprox in *. destruct H. destruct H. intuition. rewrite H2. eapply rat_le_1. eapply Nat.le_trans. eapply pred_count_le_length. eapply H. erewrite <- rel_map_length; eauto. rewrite getAllBlists_length. reflexivity. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat