proposition: Lemma row_lt_by_pos Z r p q: is_row r -> p < size r -> q < size r -> (nth Z r p < nth Z r q)%O -> p < q.
proof: Proof. Proof using. rewrite lt_neqAle. exact: (sorted_lt_by_pos (@le_trans _ T) (@le_refl _ T) (@le_anti _ T)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted