proposition: Lemma div2_grows : forall n m, m <= n -> Nat.div2 m <= Nat.div2 n.
proof: Proof. Proof using. nat_comp_to_peano. induction n using peano_induction. introv Le. destruct~ m. simpl. lia. destruct~ n. simpl. lia. destruct~ m. simpl. lia. destruct~ n. simpl. lia. simpl. forwards~: H n m. nat_math. nat_math. nat_math. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat