- ∀O:pordered_set.∀a:sequence O.∀l:O.
- is_lower_bound O a l → is_upper_bound (reverse_pordered_set O) a l.
-intros (O a l H); unfold; intros (n); unfold reverse_pordered_set;
-unfold reverse_excedence; simplify; fold unfold le (le ? l (a n)); apply H;
+ ∀O:excess.∀a:sequence O.∀l:O.
+ is_lower_bound O a l → is_upper_bound (reverse_excess O) a l.
+intros (O a l H); unfold; intros (n); unfold reverse_excess;
+unfold reverse_excess; simplify; fold unfold le (le ? l (a n)); apply H;