fact: Hypothesis All_strictly_monotonic : forall f, match get_arity f with | 0 => True | _ => monotonic_strict_aux false (get_arity f) (Pols f) (Pols f) end.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)