proposition: Lemma max_le_1 : forall a b, a <= max a b.
proof: Proof. unfold max. intros. rewrite <- compare_reflectR. case (trichotomy_inf a b);auto with T1. destruct s;auto with T1. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List