proposition: Lemma comp_comp : forall dpR R comp, (forall uv uv', are_connected dpR R uv uv' -> comp uv <= comp uv') -> forall uv uv', comp uv <> comp uv' -> ~ (refl_trans_clos (are_connected dpR R) uv uv' /\ refl_trans_clos (are_connected dpR R) uv' uv).
proof: Proof. intros dpR R comp H1 uv uv' H2 [H3 H4]. apply H2; clear H2. destruct H3 as [a | a b H3]. apply eq_refl. destruct H4 as [a | a b H4]. apply eq_refl. apply Nat.le_antisymm. clear H4; induction H3 as [a b H3 | a b c H3 H4]. apply H1; assumption. apply Nat.le_trans with (comp b); [ apply H1 | ]; assumption. clear H3; induction H4 as [a b H3 | a b c H3 H4]. apply H1; assumption. apply Nat.le_trans with (comp b); [ apply H1 | ]; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)