proposition: Lemma ord_1_0 (i : 'I_1) : i = ord0.
proof: Proof. by case: i => [[]] // HH; apply /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype bigop matrix) CoqEAL(hrel param refinements seqmx seqpoly)