proposition: Lemma red_normal : forall u v, red u v -> normal u -> u = v.
proof: Proof. simple induction 1; auto with coc core arith sets; intros. absurd (red1 u N); auto with coc core arith sets. absurd (red1 P N); auto with coc core arith sets. elim (H1 H3). unfold not in |- *; intro; apply (H3 N); auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations