proposition: Lemma shiftinv_pos_homo pos : {homo shiftinv_pos pos : i j / i <= j}.
proof: Proof. Proof using. move=> i j Hij; rewrite /shiftinv_pos; case (ltnP j pos) => Hj. - by rewrite (leq_ltn_trans Hij Hj). - case (ltnP i pos) => Hi. + by have:= leq_trans Hi Hj; case j. + by case: i Hij {Hj Hi} => //= i; case: j. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools