Commit d568ecd2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add support for some improper integrals with a singularity at zero.

parent daa6c66e
This diff is collapsed.
......@@ -72,7 +72,7 @@ Goal
(at_right 0) (at_point 1) = 1/32.
Proof.
refine ((fun H => Rle_antisym _ _ (proj2 H) (proj1 H)) _).
interval.
integral.
Qed.
Goal
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment