(* *)
(**************************************************************************)
-include "ordered_uniform.ma".
-include "russell_support.ma".
+include "dama/ordered_uniform.ma".
+include "dama/russell_support.ma".
(* Definition 3.5 *)
alias num (instance 0) = "natural number".
|7:apply (ge_reflexive (l : hos_carr (os_r C)));
|8:apply (H12 i);
|6:change with (a i ≤ a (m O));
- apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]
+ apply (trans_decreasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]
clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
generalize in match (refl_eq nat (m p));
generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;