proposition: Lemma is_row_set_nth l r pos : is_row r -> (l < nth l r pos)%O -> (forall n : nat, (l < nth l r n)%O -> pos <= n) -> is_row (set_nth l r pos l).
proof: Proof. Proof using. move=> /is_row1P Hrow Hl Hmin. apply/(is_row1P l) => i. rewrite (lock (i.+1)) !nth_set_nth /=; unlock. case: (ltnP pos (size r)) Hl => [Hpos Hl |HH]; first last. by rewrite (nth_default l HH) ltxx. rewrite size_set_nth maxnC /maxn. move: Hpos; rewrite leqNgt; move/negbTE => -> Hi1lt. case eqP => Hipos; case eqP => Hi1pos. - exact: le_refl. - by apply: ltW; apply: (lt_le_trans Hl); rewrite -Hipos; apply: Hrow. - move: {Hmin} (contra (Hmin i)); rewrite -leNgt -ltnNge; apply. by rewrite Hi1pos leqnn. - exact: Hrow. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted