proposition: Lemma adcBmain_nat n : forall b (p1 p2: BITS n), adcBmain b p1 p2 = #(b + toNat p1 + toNat p2).
proof: Proof. induction n. + move => b p1 p2. rewrite 2!toNatNil. by destruct b. + move => b. case/tupleP => [b1 p1]. case/tupleP => [b2 p2]. rewrite /fromNat-/fromNat/=. rewrite !theadCons !beheadCons !toNatCons !oddD !odd_double /=. case e: (fullAdder b b1 b2) => [carry' b0]. specialize (IHn carry' p1 p2). rewrite IHn /= addnA. assert (b0 = odd b (+) (odd b1 (+) false) (+) (odd b2 (+) false)). rewrite /fullAdder in e. destruct b; destruct b1; destruct b2; inversion e; subst; done. rewrite -H. assert (carry' + toNat p1 + toNat p2 = (b + (b1 + (toNat p1).*2) + b2 + (toNat p2).*2)./2). rewrite addnA (addnC _ b2) -!addnA -doubleD !addnA. rewrite /fullAdder in e. destruct b; destruct b1; destruct b2; inversion e; subst; simpl; by (try rewrite uphalf_double; try rewrite half_double). rewrite H0. by apply val_inj. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)