proposition: Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z.
proof: Proof. intros n m; unfold is_lt, Z.lt , Z.le, Z.compare. rewrite Pos.compare_antisym. case (m ?= n); simpl; auto; intros HH; discriminate HH. Qed.
imports: ZArith Lia