proposition: Lemma compnref_rev c1 c2 : (rev_intcompn c1 <= rev_intcompn c2 :> 'CRef)%O = (c1 <= c2)%O.
proof: Proof. suff impl c c' : (c <= c')%O -> (rev_intcompn c <= rev_intcompn c' :> 'CRef)%O. by apply/idP/idP=> /impl //; rewrite !rev_intcompnK. rewrite !leEcompnref => /subdescsetP[s /= Hc Hd]. apply/subdescsetP; exists (rev (map rev s)) => /=. - rewrite Hc map_rev -map_comp; congr rev; apply eq_map => t /=. by rewrite sumn_rev. - by rewrite -rev_flatten Hd. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype