proposition: Lemma beq_eq : forall n1 n2, beq n1 n2 = isTrue (n1 = n2).
proof: Proof. Proof using. intros n1. induction n1; intros; destruct n2; simpl; rew_bool_eq; auto_false. rewrite IHn1. extens. rew_istrue. nat_math. Qed.
imports: Coq.Arith.Arith Coq.micromega.Lia TLC(LibTactics LibReflect LibBool LibOperation LibRelation LibOrder)