proposition: Lemma red_red_prod : forall u u0 v v0, red u u0 -> red v v0 -> red (Prod u v) (Prod u0 v0).
proof: Proof. simple induction 1. simple induction 1; intros; auto with coc core arith sets. apply trans_red with (Prod u P); auto with coc core arith sets. intros. apply trans_red with (Prod P v0); auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations