Formal verification using interactive theorem provers have been noticed as a method of verification of proofs that are too big for humans to check the validity of them. In this work, we verify validity of Robertson-type uncertainty relation using proof assistant Coq toward verifying unconditional security of quantum key distributions.