terminals s

syntax

n ::= 0
    | s n


judgment gt: n > n

------- gt-one
s n > n

n1 > n2
--------- gt-more
s n1 > n2


lemma all-gt-zero:
	forall n
	exists s n > 0 .
	
	_: s n > 0 by induction on n:
		case 0 is
			_: s 0 > 0 by rule gt-one
		end case
		
		case s n1 is
			g: s n1 > 0 by induction hypothesis on n1
			_: s s n1 > 0 by rule gt-more on g
		end case
	end induction
end lemma

theorem gt-implies-gt-succ:
	forall g: n1 > n2
	exists s n1 > s n2 .
	
	_: s n1 > s n2 by induction on g:
		case rule
			------------ gt-one
			_: s n2 > n2
		is
			_: s s n2 > s n2 by rule gt-one
		end case
		
		case rule
			g1: n11 > n2
			------------- gt-more
			_: s n11 > n2
		is
			g2: s n11 > s n2 by induction hypothesis on g1
			_: s s n11 > s n2 by rule gt-more on g2
		end case
	end induction
end theorem