proposition: Lemma I_i_wf: @well_founded 'I_i (<%O).
proof: Proof. case => m Hm; rewrite ltEord. apply (Acc_inverse_image 'I_i nat _ (nat_of_ord (n:=i)) _ (wf_ltn (Ordinal Hm))). Qed.
imports: mathcomp(all_ssreflect zify) mathcomp(fintype) Coq(Logic.Eqdep_dec) Coq(Wellfounded.Inclusion Wf_nat Inverse_Image)