Theorem zlenlt ≪ | index | src | ≫

theorem zlenlt (a b: nat): $ a <=Z b <-> ~b 
    

      

        
Step
Hyp
Ref
Expression
        

          
1
          

          
biid
          
a <=Z b <-> a <=Z b
        
        

          
2
          
1
          
conv zle
          
a <=Z b <-> ~b <Z a
        
      
    
    
Axiom use
    axs_prop_calc
     (ax_1,
      ax_2,
      ax_3,
      ax_mp)