DEFINITION leq_asucc_false()
TYPE =
       ∀g:G.∀a:A.(leq g (asucc g a) a)→∀P:Prop.P
BODY =
Show proof