lapply (isrt_inj โฆ Hn2 H2) -c2 #H destruct //
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-.
+
(* Properties with shift ****************************************************)
lemma max_shift: โc1,c2. ((โ*c1) โจ (โ*c2)) = โ*(c1โจc2).
* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
<shift_rew <shift_rew <shift_rew <max_rew //
qed.
+
+(* Inversion lemmaswith shift ***********************************************)
+
+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-.