proposition: Lemma are_bits : forall (f:t->bool), Proper (eq==>Logic.eq) f -> ((exists n, f === testbit n) <-> (exists k, forall m, k<=m -> f m = false)).
proof: Proof. intros f Hf. split. - intros (a,H). exists (S (log2 a)). intros m Hm. apply le_succ_l in Hm. rewrite H, bits_above_log2; trivial using lt_succ_diag_r. - intros (k,Hk). revert f Hf Hk. induct k. + intros f Hf H0. exists 0. intros m. rewrite bits_0, H0; trivial. apply le_0_l. + intros k IH f Hf Hk. destruct (IH (fun m => f (S m))) as (n, Hn). * solve_proper. * intros m Hm. apply Hk. now rewrite <- succ_le_mono. * { exists (f 0 + 2*n). intros m. destruct (zero_or_succ m) as [Hm|(m', Hm)]; rewrite Hm. - symmetry. apply add_b2n_double_bit0. - rewrite Hn, <- div2_bits. rewrite mul_comm, div_add, b2n_div2, add_0_l; trivial. order'. } Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog