proposition: Theorem getSupport_not_In_lowDistApprox : forall n (A : Set)(c : Comp A)(a : A) r, ~In a (getSupport c) -> lowDistApprox c a n r -> r == 0.
proof: Proof. intuition. destruct H0. destruct H0. intuition. specialize (@pred_count_eq_0 (comp_answer A) Blist (getAllBlists n) x (evalDet c) (eq (ca_done a)) x0); intuition. rewrite H2 in H3. rewrite H3. apply rat_num_0. intuition. subst. eapply H. eapply getSupport_In_evalDet; eauto. trivial. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat