proposition: Lemma Zle_neq_Zlt : forall a b : Z, (a <= b)%Z -> b <> a -> (a < b)%Z.
proof: Proof. intros a b H H0. case (Z_le_lt_eq_dec _ _ H); trivial. intro; apply False_ind; apply H0; symmetry in |- *; assumption. Qed.
imports: Coq(Lia)