proposition: Lemma reltoI a b : relto (predI a b) r =2 relto a (relto b r).
proof: Proof. by move=> x y; rewrite /= andbA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin