proposition: Lemma canon_id : forall x, (invariant canon canon) x.
proof: Proof. move=> x /=; rewrite /canon (@eq_choose _ _ (eC x)). by rewrite (@choose_id _ (eC x) _ x) ?chooseP ?equiv_refl. by move=> y; apply: equiv_ltrans; rewrite equiv_sym /= chooseP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)