fact: Definition sbbB {n} borrow (arg1 arg2: BITS n) := let (carry, res) := eta_expand (adcB (~~borrow) arg1 (invB arg2)) in (~~carry, res).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq tuple) spec