proposition: Lemma iter_le_fast_exp2_same n x y : iter_le_fast n x y <-> iter_le ((exp2 n)-1) x y.
proof: Proof. rewrite iter_le_spec, iter_le_fast_spec. split; intro; destruct H as [p]; exists p; split_all; ded (exp2_pos n); lia. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)