(* Properties ***************************************************************)
+fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+// qed-.
+
lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
/3 width=1 by monotonic_le_minus_l/ qed.
#B #f #b #l elim l -l normalize //
qed.
+lemma iter_plus: ∀B:Type[0]. ∀f:B→B. ∀b,l1,l2. f^(l1+l2) b = f^l1 (f^l2 b).
+#B #f #b #l1 elim l1 -l1 normalize //
+qed.
+
(* Trichotomy operator ******************************************************)
(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)