proposition: Lemma clock_inc: forall (h: list Label)(s s': State), step_star s h s' -> (forall n, let c := (clock_state (node_states s n)) in let c' := (clock_state (node_states s' n)) in c <= c').
proof: Proof. intros. induction H. subst c. subst c'. apply Nat.le_refl. rename c' into c''. pose (c' := clock_state (node_states s2 n)). assert (c' <= c''). inversion H0. subst c'. subst c''. subst s2. subst s3. simpl. unfold override. destruct (eq_nat_dec n n0). simpl. rewrite Nat.add_comm. simpl. apply Nat.le_succ_diag_r. apply Nat.le_refl. subst c'. subst c''. subst s2. subst s3. simpl. unfold override. destruct (eq_nat_dec n n0). simpl. apply Nat.le_refl. apply Nat.le_refl. subst c'. subst c''. subst s2. subst s3. simpl. unfold override. destruct (eq_nat_dec n n0). simpl. apply Nat.le_refl. apply Nat.le_refl. subst c'. subst c''. subst s2. subst s3. simpl. unfold override. destruct (eq_nat_dec n n0). simpl. apply Nat.le_refl. apply Nat.le_refl. eapply Nat.le_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)