proposition: Lemma isEmptyMeansInf: forall l, isEmpty l = Vone <-> Forall (fun x => x > inf) l.
proof: Proof. intros. split; intros. - induction l; trivial. simpl in H. destruct (Z_lt_dec a (inf+1)); [inversion H|]. specialize (IHl H). apply Forall_cons; trivial. lia. - induction l; trivial. simpl. destruct (Z_lt_dec a (inf+1)). 2: { apply IHl. rewrite Forall_forall; intros. rewrite Forall_forall in H. simpl in H. apply H. right; trivial. } exfalso. rewrite Forall_forall in H. assert (In a (a :: l)) by (apply in_eq). specialize (H _ H0). lia. Qed.
imports: VST.floyd.proofauto