proposition: Lemma inductively_barred_at_monotone : forall P l n n', n' <= n -> inductively_barred_at P n' l -> inductively_barred_at P n l.
proof: Proof. intros * Hle Hbar. induction Hbar in n, l, Hle, Hbar |- *. - apply now_at; auto. - destruct n; [apply Nat.nle_succ_0 in Hle; contradiction|]. apply Nat.succ_le_mono in Hle. apply propagate_at; auto. Qed.
imports: WeakFan List Arith Compare_dec