proposition: Lemma ord1 : all_equal_to (0 : 'I_1).
proof: Proof. exact: ord1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)