Inversion H
 
 
Constructores  LeS :  
(n:nat)(m:nat)(Le n m)->(Le (S n) (S m)) 
 
Unificación (Le (S n) m) 
---------------- 
(Le (S n) (S m))
{n0=n,(S m0)=m}
Premisa 
Hipótesis		 (Le n m) 
(Le n m0)
Subobjetivo (P n (S m0))
 
 
 
 
ejemplo < Inversion H. 
1 subgoal 

  n : nat 
  m : nat 
  H : (Le (S n) m) 
  n0 : nat 
  m0 : nat 
  H0 : n0=n 
  H2 : (S m0)=m 
  H1 : (Le n m0) 
  ============================ 
   (P n (S m0))

 O alternativamente: 

ejemplo < Inversion_clear H. 
1 subgoal 

  n : nat 
  m : nat 
  m0 : nat 
  H0 : (Le n m0) 
  ============================ 
   (P n (S m0))