我想在 Coq 中定义一个小记录，其中还包括某些条件。此外，我想要一个定义来以简单的方式创建记录。这是我的方法：
Require Import Arith.
(* Define the qn record with conditions for q and n *)
Record qn := {
q : nat;
q_ge_2 : leb 2 q = true; (* Ensuring q is greater or equal than 2 *)
n : nat;
n_ge_1 : leb 1 n = true (* Ensuring n is greater or equal than 1 *)
}.
(* A support function to create instances of qn more conveniently *)
Definition make_qn (q n: nat) (Hq : leb 2 q = true) (Hn : leb 1 n = true) : qn :=
{| q := q; q_ge_2 := Hq; n := n; n_ge_1 := Hn |}.
(* Examples of qn *)
Example qn_example1 : qn := make_qn 2 1 (eq_refl true) (eq_refl true).
Example qn_example2 : qn := make_qn 3 5 (eq_refl true) (eq_refl true).
Example qn_example3 : qn := make_qn 4 2 (eq_refl true) (eq_refl true).
我已经尝试了一些不同的方法 - 也定义了 qn 记录，例如使用 Prop 而不是 bool。
有没有办法简化make_qn定义直接包含证明？例如使用它就像
Example qn_simple1 : qn := make_qn 2 1