proposition: Lemma lowDistApprox_Rnd_lt : forall n1 n2 a r, lowDistApprox (Rnd n1) a n2 r -> n2 < n1 -> r == 0.
proof: Proof. intuition. unfold lowDistApprox in *. destruct H. destruct H. intuition. rewrite H3. assert (x0 = O). eapply pred_count_func. eauto. eapply pred_count_eq_none; intuition. subst. assert (x = (listRepeat (@ca_eof (Bvector n1)) (length (getAllBlists n2)))). eapply rel_map_func. eauto. eapply rel_map_listRepeat. intuition. econstructor. econstructor. eauto. simpl. rewrite shiftOut_lt. econstructor. erewrite getAllBlists_In_length. eauto. trivial. intuition. eapply evalDet_func; eauto. subst. apply in_listRepeat_inv in H2. discriminate. subst. eapply rat_num_0. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat