(*** sle_tls *)
lemma gr_sle_tls:
- â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 â\88\80n. ⫱*[n] f1 â\8a\86 ⫱*[n] f2.
+ â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 â\88\80n. â«°*[n] f1 â\8a\86 â«°*[n] f2.
#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n
/2 width=5 by gr_sle_tl/
qed.