proposition: Theorem le_max : forall n p, n <= p -> max n p = p.
proof: Proof. intros n p ; unfold max ; case (le_lt_dec n p); simpl. - trivial. - intros; absurd (p < p); eauto with arith. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec