fact: Fixpoint adcBmain n carry : BITS n -> BITS n -> BITS n.+1 := if n is _.+1 then fun p1 p2 => let (p1,b1) := eta_expand (splitlsb p1) in let (p2,b2) := eta_expand (splitlsb p2) in let (carry',b) := fullAdder carry b1 b2 in joinlsb (adcBmain carry' p1 p2, b) else fun _ _ => singleBit carry.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq tuple) spec