proposition: Lemma log2_Zle :forall a b, Zpos a <= Zpos b -> log2 a <= log2 b.
proof: Proof. Proof with zsimpl;try lia. induction a;destruct b;zsimpl;intros;simpl ... assert (log2 a <= log2 b) ... apply IHa ... assert (log2 a <= log2 b) ... apply IHa ... assert (log2 a <= log2 b) ... apply IHa ... assert (log2 a <= log2 b) ... apply IHa ... Qed.
imports: ZArith Lia ZCmisc