proposition: Lemma cast_nat_posK n : n > 0 -> cast_pos_nat (cast_nat_pos n) = n.
proof: Proof. by rewrite /cast_pos_nat /cast_nat_pos val_insubd=> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements pos hrel poly_op)