@(\ 5a href="cic:/matita/arithmetics/nat/le_gen.def(1)"\ 6le_gen\ 5/a\ 6 ? n1) #i generalize in match p2; (elim i)
[(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
>\ 5a href="cic:/matita/arithmetics/bigops/bigop_Sfalse.def(3)"\ 6bigop_Sfalse\ 5/a\ 6
- [@(Hind ? (\ 5a href="cic:/matita/arithmetics/nat/le_O_n.def(2)"\ 6le_O_n\ 5/a\ 6 ?)) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/bigops/sub_hkO.def(4)"\ 6sub_hkO\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | @(\ 5a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"\ 6transitive_sub\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"\ 6sub_lt\ 5/a\ 6 …) sub2) //]
+ [@(Hind ? (\ 5a href="cic:/matita/arithmetics/nat/le_O_n.def(2)"\ 6le_O_n\ 5/a\ 6 ?)) [@\ 5a href="cic:/matita/arithmetics/bigops/sub_hkO.def(4)"\ 6sub_hkO\ 5/a\ 6 % | @(\ 5a href="cic:/matita/arithmetics/bigops/transitive_sub.def(4)"\ 6transitive_sub\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/bigops/sub_lt.def(5)"\ 6sub_lt\ 5/a\ 6 …) sub2) //]
|@(\ 5a href="cic:/matita/arithmetics/bigops/sub0_to_false.def(4)"\ 6sub0_to_false\ 5/a\ 6 … sub2) //
]
|#n #Hind #p2 #ltn #sub1 #sub2 (cut (n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6n1)) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"\ 6le_plus_b\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] #len