proposition: Lemma red_conv : forall M N, red M N -> conv M N.
proof: Proof. simple induction 1; auto with coc core arith sets. intros; apply trans_conv_red with P; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations