proposition: Lemma abstrX1 (i : nat) : abstrX i 1%T = [::1%T].
proof: Proof. done. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)