+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-.
+