fact: Fixpoint monotonic_aux n : Pol_type n -> Pol_type n -> Prop:= match n as m return Pol_type m -> Pol_type m -> Prop with | 0 => fun a b => Ale a b | S n => fun P1 P2 => forall x1 x2, (A0<=x1) /\ (x1 <= x2) -> monotonic_aux n (P1 x1) (P2 x2) end.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)