proposition: Fact int_num_subring : subring_closed int_num.
proof: Proof. split=> // u v /[!intrE] /orP[]/natrP[n] + /orP[]/natrP[m]; rewrite ?opprB. - move=> -> ->. by case: (leqP n m) => [|/ltnW] ?; apply/orP; [right|left]; rewrite -mulrnBr. - by move=> -> ->; rewrite -mulrnDr natr_nat. - by move=> -> ->; rewrite -mulrnDr natr_nat orbT. - rewrite -[u in u - v]opprK -[v in v - u]opprK => -> ->. by case: (leqP n m) => [|/ltnW] ?; apply/orP; [left|right]; rewrite addrC -mulrnBr. - by move=> -> ->; rewrite -natrM natr_nat. - by rewrite -mulrN => -> ->; rewrite -natrM natr_nat orbT. - by rewrite -mulNr => -> ->; rewrite -natrM natr_nat orbT. - by rewrite -mulrNN => -> ->; rewrite -natrM natr_nat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)