proposition: Lemma add_test_constraint_right_monotonic : forall neg v1 v2 v1' v2' v v', add_test_constraint_right neg v1 v2 = Some v -> add_test_constraint_right neg v1' v2' = Some v' -> thinner v1 v1' -> thinner v2 v2' -> thinner v v'.
proof: Proof. intros [|]. apply add_test_constraint_right_true_monotonic. apply add_test_constraint_right_false_monotonic. Qed.
imports: ZArith List Lia