proposition: Lemma div2_lt : forall n m, m <= n -> n > 0 -> Nat.div2 m < n.
proof: Proof. Proof using. nat_comp_to_peano. introv Le Gt. forwards: Nat.div2_decr m (n-1). lia. lia. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat