proposition: Lemma lor_le x y : (y <=? x lor y)%uint63 = true.
proof: Proof. generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y. unfold wB; elim size. - replace (2^Z_of_nat 0) with 1%Z; auto with zarith. intros x y Hx Hy; replace x with 0%uint63. + replace y with 0%uint63; auto. apply to_Z_inj; rewrite to_Z_0; auto with zarith. + apply to_Z_inj; rewrite to_Z_0; auto with zarith. - intros n IH x y; rewrite inj_S. unfold Z.succ; rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith. intros Hx Hy. rewrite leb_spec. rewrite -> (to_Z_split y) at 1; rewrite (to_Z_split (x lor y)). assert (φ (y>>1) <= φ ((x lor y) >> 1)). + rewrite -> lor_lsr, <-leb_spec; apply IH. * rewrite -> lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. * rewrite -> lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. + assert (φ (bit y 0) <= φ (bit (x lor y) 0)); auto with zarith. rewrite lor_spec; do 2 case bit; try discriminate. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63