proposition: Lemma add3_bits_div2 : forall (a0 b0 c0 : bool), (a0 + b0 + c0)/2 == nextcarry a0 b0 c0.
proof: Proof. assert (H : 1+1 == 2) by now nzsimpl'. intros [|] [|] [|]; simpl; rewrite ?add_0_l, ?add_0_r, ?H; (apply div_same; order') || (apply div_small; order') || idtac. symmetry. apply div_unique with 1. { order'. } now nzsimpl'. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog