โงโง ๐๐โชn,c1โซ & ๐๐โชn,c2โซ.
#n #c1 #c2 #H #Hc12
elim (isrt_inv_max โฆ H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
โงโง ๐๐โชn,c1โซ & ๐๐โชn,c2โซ.
#n #c1 #c2 #H #Hc12
elim (isrt_inv_max โฆ H) -H #n1 #n2 #Hc1 #Hc2 #H destruct