proposition: Lemma lowDistApproxFromTree_eq_0 : forall (A : Set)(eqd : eq_dec A)(t : DistApproxTree A) a, ~In a (getTreeSupport eqd t) -> lowDistApproxFromTree eqd t a == 0.
proof: Proof. induction t; intuition; simpl in *. destruct o. destruct (eqd a a0); subst. exfalso. eapply H. simpl. intuition. intuition. intuition. rewrite IHt1. rewrite IHt2. rewrite ratMult_0_l. rewrite <- ratAdd_0_r. intuition. intuition. eapply H. unfold getTreeSupport in *. simpl. eapply in_getUnique. eapply in_or_app. right. eapply in_getUnique_if. eauto. intuition. eapply H. unfold getTreeSupport in *. simpl. eapply in_getUnique. eapply in_or_app. left. eapply in_getUnique_if. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat