proposition: Lemma if_nth s b n : b || (size s <= n) -> (if b then nth s n else x0) = nth s n.
proof: Proof. by case: leqP; case: ifP => //= *; rewrite nth_default. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)