proposition: Theorem evalDist_1_0 : forall (A : Set){eqd : EqDec A}(c : Comp A) a, well_formed_comp c -> evalDist c a == 1 -> (forall b, b <> a -> evalDist c b == 0).
proof: Proof. intuition. eapply leRat_impl_eqRat. eapply (leRat_ratAdd_same_r (evalDist c a)). eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite H0. eapply ratAdd_0_l. } assert ( evalDist c b + evalDist c a == sumList (a :: b :: nil)%list (evalDist c)). repeat rewrite sumList_cons. rewrite ratAdd_comm. eapply ratAdd_eqRat_compat; intuition. rewrite ratAdd_0_r at 1. eapply ratAdd_eqRat_compat; intuition. unfold sumList; simpl; intuition. rewrite H2. eapply evalDist_le_1_gen; intuition. econstructor. simpl; intuition. econstructor; simpl; intuition. econstructor. eapply rat0_le_all. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec