Skip to content

Commit c0a6954

Browse files
committed
1 parent 5025b7e commit c0a6954

26 files changed

+436
-436
lines changed

src/FCF/Bernoulli.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ Theorem Bernoulli_correct :
4242
apply filter_In in H0.
4343
intuition.
4444
exfalso.
45-
destruct (lt_dec a n); intuition.
45+
destruct (lt_dec a n); intuition auto with *.
4646

4747
eapply sumList_0.
4848
intros.
@@ -88,7 +88,7 @@ Theorem Bernoulli_correct_complement :
8888
eapply eqRat_trans.
8989
eapply evalDist_complement.
9090
eapply Bernoulli_wf.
91-
eapply ratSubtract_eqRat_compat; intuition.
91+
eapply ratSubtract_eqRat_compat; intuition auto with *.
9292
eapply Bernoulli_correct.
9393
trivial.
9494
Qed.

0 commit comments

Comments
 (0)