1
$\begingroup$

Im trying to prove:

Local Open Scope ring_scope.
Local Open Scope ereal_scope.
Local Open Scope ldl_scope.
Context {R : realType}.

Lemma aku : forall x1 x2 : \bar R, (x1 < x2) -> (x1 <= x2).

But I don't have the first clue on how to start.

Improve this question
$\endgroup$
1
  • 4
    $\begingroup$ Please give us a minimal working example, in particular one where your Imports appear (currently, trying to run your example as is gives an error on line 1). Otherwise, we are lacking context to help you. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Sep 23 at 8:43

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.