-lemma isrt_inv_max_shift_sn: โn,c1,c2. ๐๐โฆn, โ*c1 โจ c2โฆ โ
- โงโง ๐๐โฆ0, c1โฆ & ๐๐โฆn, c2โฆ.
-#n #c1 #c2 #H
-elim (isrt_inv_max โฆ H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
-elim (isrt_inv_shift โฆ Hc1) -Hc1 #Hc1 * -n1
-/2 width=1 by conj/
-qed-.
-
-lemma isrt_inv_max_eq_t: โn,c1,c2. ๐๐โฆn, c1 โจ c2โฆ โ eq_t c1 c2 โ
- โงโง ๐๐โฆn, c1โฆ & ๐๐โฆn, c2โฆ.
-#n #c1 #c2 #H #Hc12
-elim (isrt_inv_max โฆ H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
-lapply (isrt_eq_t_trans โฆ Hc1 โฆ Hc12) -Hc12 #H
-<(isrt_inj โฆ H โฆ Hc2) -Hc2
-<idempotent_max /2 width=1 by conj/
-qed-.
-