proposition: Lemma parent_cr : forall (c0 : Config) (s1 s2 : Site), legal c0 -> parent c0 s1 s2 -> dt c0 s1 < dt c0 s2.
proof: Proof. intros c0 s1 s2 H; elim H. intros; apply init_parent_cr; trivial. simple induction t; unfold transition in |- *; intros. apply copy_trans_parent_cr; trivial. apply rdec_trans_parent_cr; trivial. apply rinc_trans_parent_cr; trivial. apply rcop1_trans_parent_cr; trivial. apply rcop2_trans_parent_cr; trivial. apply rcop3_trans_parent_cr. apply (first_copy_diff_site c); trivial. trivial. exact (ancestor_rt c H0). intros; apply le_dt_time; trivial. trivial. trivial. apply del_trans_parent_cr; trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc