proposition: Lemma Zlt_def (x y : Z) : (x <? y)%Z = (y != x) && (x <=? y)%Z.
proof: Proof. Admitted. Lemma Zle_total : forall m n : Z, (m <=? n)%Z || (n <=? m)%Z. Proof. Admitted. Lemma Z_display : Datatypes.unit. Proof. exact: tt. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith