proposition: Theorem getSupport_In_evalDist : forall (A : Set)(c : Comp A)(a : A), In a (getSupport c) <-> ~(evalDist c a == 0).
proof: Proof. induction c; simpl in *; intuition. subst. destruct (e a0 a0). eapply rat1_ne_rat0. trivial. congruence. destruct (e a a0); subst. intuition. right. intuition. apply in_getUnique_if in H0. apply in_flatten in H0. destruct H0. intuition. apply in_map_iff in H2. destruct H2. intuition. eapply sumList_0 in H1; eauto. apply ratMult_0 in H1; intuition. eapply IHc; eauto. subst. eapply H; eauto. apply (in_getUnique (flatten (map (fun b : B => getSupport (c0 b)) (getSupport c)))). apply in_flatten. apply sumList_nz in H0. destruct H0. intuition. apply ratMult_nz in H2. intuition. econstructor. split. eapply in_map_iff. econstructor. split. eapply eq_refl. eapply H1. eapply H. eauto. eapply in_getAllBvectors. apply ratMult_0 in H0. intuition. apply ratMult_0 in H1. intuition. unfold indicator in *. case_eq (b a); intuition. rewrite H1 in H0. eapply rat1_ne_rat0. trivial. eapply filter_not_In. eauto. eauto. eapply ratInverse_nz; eauto. eapply IHc. eapply filter_In. eauto. trivial. apply ratMult_nz in H. intuition. apply ratMult_nz in H0. intuition. unfold indicator in *. case_eq (b a); intuition; rewrite H0 in H. eapply filter_In. intuition. eapply IHc. trivial. exfalso. intuition. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec