proposition: Lemma eqSub (n m : nat) : int_of_Z (if (m <= n)%C then Zpos pos (n - m)%N else Zneg nat (cast (m - n)%N)) = (Posz n) - (Posz m).
proof: Proof. have [mn|nm] /= := leqP m n. have := mn. rewrite -[((_<=_)%N)]/(_<=_)%C => ->. by rewrite /= -subzn. rewrite [((_<=_)%C)]/(_<=_)%N ifN_eq=> /=. by rewrite insubdK -?topredE /= ?subn_gt0 // -?subzn 1?ltnW // opprB. by have := nm; rewrite lt0n_neq0 // subn_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset bigop order) mathcomp(ssralg zmodp ssrnum ssrint) CoqEAL(hrel param refinements pos)