proposition: Lemma shift_pos_mono pos : {mono shift_pos pos : i j / i <= j}.
proof: Proof. Proof using. rewrite /shift_pos => i j; case (ltnP j pos) => Hj. - case (leqP i j) => Hij; first by rewrite (leq_ltn_trans Hij Hj) Hij. rewrite leqNgt (leq_trans Hij) //. by case: ltnP. - case (leqP i j) => Hij. by rewrite (leq_trans (n := i.+1)) //; case ltnP. rewrite ltnNge (ltnW (leq_ltn_trans Hj Hij)) /=. by rewrite ltnNge Hij. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools