Ssreflect Users Discussion List

[Laurent Thery <>]

Hi,

I am trying to build a tactic for the ratioal that looks
something like repeat (apply: H1 || apply: H2 ...)
but the tactic is unusual because the applications when failing take a 
very long time.

Here is an example:

==============================

From mathcomp Require Import all_ssreflect all_algebra.

Import GRing.Theory Num.Theory.
Open Scope ring_scope.

Goal (forall x y : rat, x * 1 <= x * 1) -> forall x y : rat, x + 10%:R <= y.
Proof.
move=> H x y.
apply: H.

=================================

Is there a work-around?

--
Laurent