n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus g (next
g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus g (next
g n0) n)) (next_plus_next g (next g n0) n))))) h)).
n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus g (next
g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus g (next
g n0) n)) (next_plus_next g (next g n0) n))))) h)).