elim (max_inv_O3 โฆ H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/
qed-.
+lemma isrt_O_inv_max: โc1,c2. ๐๐โฆ0, c1 โจ c2โฆ โ โงโง ๐๐โฆ0, c1โฆ & ๐๐โฆ0, c2โฆ.
+#c1 #c2 #H
+elim (isrt_inv_max โฆ H) -H #n1 #n2 #Hn1 #Hn2 #H
+elim (max_inv_O3 โฆ H) -H #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
+
lemma isrt_inv_max_O_dx: โn,c1,c2. ๐๐โฆn, c1 โจ c2โฆ โ ๐๐โฆ0, c2โฆ โ ๐๐โฆn, c1โฆ.
#n #c1 #c2 #H #H2
elim (isrt_inv_max โฆ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct