Ssreflect Users Discussion List

[Jean-Jacques Levy <>]

Beginner's question: why I get 2 different answers to following inputs ? -JJ-

> elim: n (n < S(n) )

2 subgoals
  
  ============================
   bool -> reflect (ev 0) (evenb 0)

subgoal 2 is:
 forall n : nat,
 (bool -> reflect (ev n) (evenb n)) -> bool -> reflect (ev n.+1) (evenb n.+1)

> elim: n (ltnSn n).

   0 < 1 -> reflect (ev 0) (evenb 0)

subgoal 2 is:
 forall n : nat,
 (n < n.+1 -> reflect (ev n) (evenb n)) ->
 n.+1 < n.+2 -> reflect (ev n.+1) (evenb n.+1)

>  elim: n (n < S(n))%coq_nat.

2 subgoals
  
  ============================
   Prop -> reflect (ev 0) (evenb 0)

subgoal 2 is:
 forall n : nat,
 (Prop -> reflect (ev n) (evenb n)) -> Prop -> reflect (ev n.+1) (evenb n.+1)