proposition: Lemma ord_sup_minimal_converse: forall (I:Type) (alpha:I->Ordinal) (beta:Ordinal), ord_sup alpha <= beta -> forall i:I, alpha i <= beta.
proof: Proof. intros. inversion H. apply inj_pair2 in H2. destruct H2. apply H3. Qed.
imports: Coq(Classical) Coq(Eqdep)