Commit 12361989 authored by Heiko Becker's avatar Heiko Becker
Browse files

Lemma to show that a point interval always contains the point

parent 11f377c2
......@@ -69,6 +69,12 @@ Definition validIntervalDiv (iv1:interval) (iv2:interval) (iv3:interval) :=
forall a b, contained a iv1 -> contained b iv2 ->
contained (a / b) iv3.
Lemma validPointInterval (a:R) :
contained a (mkInterval a a).
Proof.
unfold contained; split; simpl; apply Req_le; auto.
Qed.
(**
Now comes the old part with the computational definitions.
Where possible within time, they are shown sound with respect to the definitions from before, where not, we leave this as proof obligation for daisy.
......
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